H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 3.079 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((index :: (Int,Int) -> Int -> Int) :: (Int,Int) -> Int -> Int)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

b@(vw,vx)

is replaced by the following term

(vw,vx)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((index :: (Int,Int) -> Int -> Int) :: (Int,Int) -> Int -> Int)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

index (vw,vx) i

| inRange (vw,vx) i

= i - vw

| otherwise

= error []

is transformed to

index (vw,vx) i = index2 (vw,vx) i

index1 vw vx i True = i - vw

index1 vw vx i False = index0 vw vx i otherwise

index0 vw vx i True = error []

index2 (vw,vx) i = index1 vw vx i (inRange (vw,vx) i)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

mainModule Main

(index :: (Int,Int) -> Int -> Int)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="index",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="index wu3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="index wu3 wu4",fontsize=16,color="burlywood",shape="triangle"];2086[label="wu3/(wu30,wu31)",fontsize=10,color="white",style="solid",shape="box"];4 -> 2086[label="",style="solid", color="burlywood", weight=9];
2086 -> 5[label="",style="solid", color="burlywood", weight=3];
5[label="index (wu30,wu31) wu4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="index2 (wu30,wu31) wu4",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="index1 wu30 wu31 wu4 (inRange (wu30,wu31) wu4)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="index1 wu30 wu31 wu4 (wu30 <= wu4 && wu4 <= wu31)",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="index1 wu30 wu31 wu4 (compare wu30 wu4 /= GT && wu4 <= wu31)",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="index1 wu30 wu31 wu4 (not (compare wu30 wu4 == GT) && wu4 <= wu31)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="index1 wu30 wu31 wu4 (not (primCmpInt wu30 wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2087[label="wu30/Pos wu300",fontsize=10,color="white",style="solid",shape="box"];11 -> 2087[label="",style="solid", color="burlywood", weight=9];
2087 -> 12[label="",style="solid", color="burlywood", weight=3];
2088[label="wu30/Neg wu300",fontsize=10,color="white",style="solid",shape="box"];11 -> 2088[label="",style="solid", color="burlywood", weight=9];
2088 -> 13[label="",style="solid", color="burlywood", weight=3];
12[label="index1 (Pos wu300) wu31 wu4 (not (primCmpInt (Pos wu300) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2089[label="wu300/Succ wu3000",fontsize=10,color="white",style="solid",shape="box"];12 -> 2089[label="",style="solid", color="burlywood", weight=9];
2089 -> 14[label="",style="solid", color="burlywood", weight=3];
2090[label="wu300/Zero",fontsize=10,color="white",style="solid",shape="box"];12 -> 2090[label="",style="solid", color="burlywood", weight=9];
2090 -> 15[label="",style="solid", color="burlywood", weight=3];
13[label="index1 (Neg wu300) wu31 wu4 (not (primCmpInt (Neg wu300) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2091[label="wu300/Succ wu3000",fontsize=10,color="white",style="solid",shape="box"];13 -> 2091[label="",style="solid", color="burlywood", weight=9];
2091 -> 16[label="",style="solid", color="burlywood", weight=3];
2092[label="wu300/Zero",fontsize=10,color="white",style="solid",shape="box"];13 -> 2092[label="",style="solid", color="burlywood", weight=9];
2092 -> 17[label="",style="solid", color="burlywood", weight=3];
14[label="index1 (Pos (Succ wu3000)) wu31 wu4 (not (primCmpInt (Pos (Succ wu3000)) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2093[label="wu4/Pos wu40",fontsize=10,color="white",style="solid",shape="box"];14 -> 2093[label="",style="solid", color="burlywood", weight=9];
2093 -> 18[label="",style="solid", color="burlywood", weight=3];
2094[label="wu4/Neg wu40",fontsize=10,color="white",style="solid",shape="box"];14 -> 2094[label="",style="solid", color="burlywood", weight=9];
2094 -> 19[label="",style="solid", color="burlywood", weight=3];
15[label="index1 (Pos Zero) wu31 wu4 (not (primCmpInt (Pos Zero) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2095[label="wu4/Pos wu40",fontsize=10,color="white",style="solid",shape="box"];15 -> 2095[label="",style="solid", color="burlywood", weight=9];
2095 -> 20[label="",style="solid", color="burlywood", weight=3];
2096[label="wu4/Neg wu40",fontsize=10,color="white",style="solid",shape="box"];15 -> 2096[label="",style="solid", color="burlywood", weight=9];
2096 -> 21[label="",style="solid", color="burlywood", weight=3];
16[label="index1 (Neg (Succ wu3000)) wu31 wu4 (not (primCmpInt (Neg (Succ wu3000)) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2097[label="wu4/Pos wu40",fontsize=10,color="white",style="solid",shape="box"];16 -> 2097[label="",style="solid", color="burlywood", weight=9];
2097 -> 22[label="",style="solid", color="burlywood", weight=3];
2098[label="wu4/Neg wu40",fontsize=10,color="white",style="solid",shape="box"];16 -> 2098[label="",style="solid", color="burlywood", weight=9];
2098 -> 23[label="",style="solid", color="burlywood", weight=3];
17[label="index1 (Neg Zero) wu31 wu4 (not (primCmpInt (Neg Zero) wu4 == GT) && wu4 <= wu31)",fontsize=16,color="burlywood",shape="box"];2099[label="wu4/Pos wu40",fontsize=10,color="white",style="solid",shape="box"];17 -> 2099[label="",style="solid", color="burlywood", weight=9];
2099 -> 24[label="",style="solid", color="burlywood", weight=3];
2100[label="wu4/Neg wu40",fontsize=10,color="white",style="solid",shape="box"];17 -> 2100[label="",style="solid", color="burlywood", weight=9];
2100 -> 25[label="",style="solid", color="burlywood", weight=3];
18[label="index1 (Pos (Succ wu3000)) wu31 (Pos wu40) (not (primCmpInt (Pos (Succ wu3000)) (Pos wu40) == GT) && Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];18 -> 26[label="",style="solid", color="black", weight=3];
19[label="index1 (Pos (Succ wu3000)) wu31 (Neg wu40) (not (primCmpInt (Pos (Succ wu3000)) (Neg wu40) == GT) && Neg wu40 <= wu31)",fontsize=16,color="black",shape="box"];19 -> 27[label="",style="solid", color="black", weight=3];
20[label="index1 (Pos Zero) wu31 (Pos wu40) (not (primCmpInt (Pos Zero) (Pos wu40) == GT) && Pos wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2101[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];20 -> 2101[label="",style="solid", color="burlywood", weight=9];
2101 -> 28[label="",style="solid", color="burlywood", weight=3];
2102[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];20 -> 2102[label="",style="solid", color="burlywood", weight=9];
2102 -> 29[label="",style="solid", color="burlywood", weight=3];
21[label="index1 (Pos Zero) wu31 (Neg wu40) (not (primCmpInt (Pos Zero) (Neg wu40) == GT) && Neg wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2103[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];21 -> 2103[label="",style="solid", color="burlywood", weight=9];
2103 -> 30[label="",style="solid", color="burlywood", weight=3];
2104[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];21 -> 2104[label="",style="solid", color="burlywood", weight=9];
2104 -> 31[label="",style="solid", color="burlywood", weight=3];
22[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (not (primCmpInt (Neg (Succ wu3000)) (Pos wu40) == GT) && Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];22 -> 32[label="",style="solid", color="black", weight=3];
23[label="index1 (Neg (Succ wu3000)) wu31 (Neg wu40) (not (primCmpInt (Neg (Succ wu3000)) (Neg wu40) == GT) && Neg wu40 <= wu31)",fontsize=16,color="black",shape="box"];23 -> 33[label="",style="solid", color="black", weight=3];
24[label="index1 (Neg Zero) wu31 (Pos wu40) (not (primCmpInt (Neg Zero) (Pos wu40) == GT) && Pos wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2105[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];24 -> 2105[label="",style="solid", color="burlywood", weight=9];
2105 -> 34[label="",style="solid", color="burlywood", weight=3];
2106[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];24 -> 2106[label="",style="solid", color="burlywood", weight=9];
2106 -> 35[label="",style="solid", color="burlywood", weight=3];
25[label="index1 (Neg Zero) wu31 (Neg wu40) (not (primCmpInt (Neg Zero) (Neg wu40) == GT) && Neg wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2107[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];25 -> 2107[label="",style="solid", color="burlywood", weight=9];
2107 -> 36[label="",style="solid", color="burlywood", weight=3];
2108[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];25 -> 2108[label="",style="solid", color="burlywood", weight=9];
2108 -> 37[label="",style="solid", color="burlywood", weight=3];
26[label="index1 (Pos (Succ wu3000)) wu31 (Pos wu40) (not (primCmpNat (Succ wu3000) wu40 == GT) && Pos wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2109[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];26 -> 2109[label="",style="solid", color="burlywood", weight=9];
2109 -> 38[label="",style="solid", color="burlywood", weight=3];
2110[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];26 -> 2110[label="",style="solid", color="burlywood", weight=9];
2110 -> 39[label="",style="solid", color="burlywood", weight=3];
27[label="index1 (Pos (Succ wu3000)) wu31 (Neg wu40) (not (GT == GT) && Neg wu40 <= wu31)",fontsize=16,color="black",shape="box"];27 -> 40[label="",style="solid", color="black", weight=3];
28[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not (primCmpInt (Pos Zero) (Pos (Succ wu400)) == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];28 -> 41[label="",style="solid", color="black", weight=3];
29[label="index1 (Pos Zero) wu31 (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];29 -> 42[label="",style="solid", color="black", weight=3];
30[label="index1 (Pos Zero) wu31 (Neg (Succ wu400)) (not (primCmpInt (Pos Zero) (Neg (Succ wu400)) == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];30 -> 43[label="",style="solid", color="black", weight=3];
31[label="index1 (Pos Zero) wu31 (Neg Zero) (not (primCmpInt (Pos Zero) (Neg Zero) == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];31 -> 44[label="",style="solid", color="black", weight=3];
32[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (not (LT == GT) && Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];32 -> 45[label="",style="solid", color="black", weight=3];
33[label="index1 (Neg (Succ wu3000)) wu31 (Neg wu40) (not (primCmpNat wu40 (Succ wu3000) == GT) && Neg wu40 <= wu31)",fontsize=16,color="burlywood",shape="box"];2111[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];33 -> 2111[label="",style="solid", color="burlywood", weight=9];
2111 -> 46[label="",style="solid", color="burlywood", weight=3];
2112[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];33 -> 2112[label="",style="solid", color="burlywood", weight=9];
2112 -> 47[label="",style="solid", color="burlywood", weight=3];
34[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (not (primCmpInt (Neg Zero) (Pos (Succ wu400)) == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];34 -> 48[label="",style="solid", color="black", weight=3];
35[label="index1 (Neg Zero) wu31 (Pos Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];35 -> 49[label="",style="solid", color="black", weight=3];
36[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) (not (primCmpInt (Neg Zero) (Neg (Succ wu400)) == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];36 -> 50[label="",style="solid", color="black", weight=3];
37[label="index1 (Neg Zero) wu31 (Neg Zero) (not (primCmpInt (Neg Zero) (Neg Zero) == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];37 -> 51[label="",style="solid", color="black", weight=3];
38[label="index1 (Pos (Succ wu3000)) wu31 (Pos (Succ wu400)) (not (primCmpNat (Succ wu3000) (Succ wu400) == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];38 -> 52[label="",style="solid", color="black", weight=3];
39[label="index1 (Pos (Succ wu3000)) wu31 (Pos Zero) (not (primCmpNat (Succ wu3000) Zero == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];39 -> 53[label="",style="solid", color="black", weight=3];
40[label="index1 (Pos (Succ wu3000)) wu31 (Neg wu40) (not True && Neg wu40 <= wu31)",fontsize=16,color="black",shape="box"];40 -> 54[label="",style="solid", color="black", weight=3];
41[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not (primCmpNat Zero (Succ wu400) == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];41 -> 55[label="",style="solid", color="black", weight=3];
42[label="index1 (Pos Zero) wu31 (Pos Zero) (not (EQ == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];42 -> 56[label="",style="solid", color="black", weight=3];
43[label="index1 (Pos Zero) wu31 (Neg (Succ wu400)) (not (GT == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];43 -> 57[label="",style="solid", color="black", weight=3];
44[label="index1 (Pos Zero) wu31 (Neg Zero) (not (EQ == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];44 -> 58[label="",style="solid", color="black", weight=3];
45[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (not False && Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];45 -> 59[label="",style="solid", color="black", weight=3];
46[label="index1 (Neg (Succ wu3000)) wu31 (Neg (Succ wu400)) (not (primCmpNat (Succ wu400) (Succ wu3000) == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];46 -> 60[label="",style="solid", color="black", weight=3];
47[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (not (primCmpNat Zero (Succ wu3000) == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];47 -> 61[label="",style="solid", color="black", weight=3];
48[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (not (LT == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];48 -> 62[label="",style="solid", color="black", weight=3];
49[label="index1 (Neg Zero) wu31 (Pos Zero) (not (EQ == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];49 -> 63[label="",style="solid", color="black", weight=3];
50[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) (not (primCmpNat (Succ wu400) Zero == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];50 -> 64[label="",style="solid", color="black", weight=3];
51[label="index1 (Neg Zero) wu31 (Neg Zero) (not (EQ == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];51 -> 65[label="",style="solid", color="black", weight=3];
52 -> 853[label="",style="dashed", color="red", weight=0];
52[label="index1 (Pos (Succ wu3000)) wu31 (Pos (Succ wu400)) (not (primCmpNat wu3000 wu400 == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="magenta"];52 -> 854[label="",style="dashed", color="magenta", weight=3];
52 -> 855[label="",style="dashed", color="magenta", weight=3];
52 -> 856[label="",style="dashed", color="magenta", weight=3];
52 -> 857[label="",style="dashed", color="magenta", weight=3];
52 -> 858[label="",style="dashed", color="magenta", weight=3];
53[label="index1 (Pos (Succ wu3000)) wu31 (Pos Zero) (not (GT == GT) && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];53 -> 68[label="",style="solid", color="black", weight=3];
54[label="index1 (Pos (Succ wu3000)) wu31 (Neg wu40) (False && Neg wu40 <= wu31)",fontsize=16,color="black",shape="box"];54 -> 69[label="",style="solid", color="black", weight=3];
55[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not (LT == GT) && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];55 -> 70[label="",style="solid", color="black", weight=3];
56[label="index1 (Pos Zero) wu31 (Pos Zero) (not False && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];56 -> 71[label="",style="solid", color="black", weight=3];
57[label="index1 (Pos Zero) wu31 (Neg (Succ wu400)) (not True && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];57 -> 72[label="",style="solid", color="black", weight=3];
58[label="index1 (Pos Zero) wu31 (Neg Zero) (not False && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];58 -> 73[label="",style="solid", color="black", weight=3];
59[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (True && Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];59 -> 74[label="",style="solid", color="black", weight=3];
60 -> 1101[label="",style="dashed", color="red", weight=0];
60[label="index1 (Neg (Succ wu3000)) wu31 (Neg (Succ wu400)) (not (primCmpNat wu400 wu3000 == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="magenta"];60 -> 1102[label="",style="dashed", color="magenta", weight=3];
60 -> 1103[label="",style="dashed", color="magenta", weight=3];
60 -> 1104[label="",style="dashed", color="magenta", weight=3];
60 -> 1105[label="",style="dashed", color="magenta", weight=3];
60 -> 1106[label="",style="dashed", color="magenta", weight=3];
61[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (not (LT == GT) && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];61 -> 77[label="",style="solid", color="black", weight=3];
62[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (not False && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];62 -> 78[label="",style="solid", color="black", weight=3];
63[label="index1 (Neg Zero) wu31 (Pos Zero) (not False && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];63 -> 79[label="",style="solid", color="black", weight=3];
64[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) (not (GT == GT) && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];64 -> 80[label="",style="solid", color="black", weight=3];
65[label="index1 (Neg Zero) wu31 (Neg Zero) (not False && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];65 -> 81[label="",style="solid", color="black", weight=3];
854[label="wu400",fontsize=16,color="green",shape="box"];855[label="wu400",fontsize=16,color="green",shape="box"];856[label="wu3000",fontsize=16,color="green",shape="box"];857[label="wu3000",fontsize=16,color="green",shape="box"];858[label="wu31",fontsize=16,color="green",shape="box"];853[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat wu38 wu39 == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="burlywood",shape="triangle"];2115[label="wu38/Succ wu380",fontsize=10,color="white",style="solid",shape="box"];853 -> 2115[label="",style="solid", color="burlywood", weight=9];
2115 -> 889[label="",style="solid", color="burlywood", weight=3];
2116[label="wu38/Zero",fontsize=10,color="white",style="solid",shape="box"];853 -> 2116[label="",style="solid", color="burlywood", weight=9];
2116 -> 890[label="",style="solid", color="burlywood", weight=3];
68[label="index1 (Pos (Succ wu3000)) wu31 (Pos Zero) (not True && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];68 -> 86[label="",style="solid", color="black", weight=3];
69[label="index1 (Pos (Succ wu3000)) wu31 (Neg wu40) False",fontsize=16,color="black",shape="box"];69 -> 87[label="",style="solid", color="black", weight=3];
70[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not False && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];70 -> 88[label="",style="solid", color="black", weight=3];
71[label="index1 (Pos Zero) wu31 (Pos Zero) (True && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];71 -> 89[label="",style="solid", color="black", weight=3];
72[label="index1 (Pos Zero) wu31 (Neg (Succ wu400)) (False && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];72 -> 90[label="",style="solid", color="black", weight=3];
73[label="index1 (Pos Zero) wu31 (Neg Zero) (True && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];73 -> 91[label="",style="solid", color="black", weight=3];
74[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (Pos wu40 <= wu31)",fontsize=16,color="black",shape="box"];74 -> 92[label="",style="solid", color="black", weight=3];
1102[label="wu400",fontsize=16,color="green",shape="box"];1103[label="wu400",fontsize=16,color="green",shape="box"];1104[label="wu31",fontsize=16,color="green",shape="box"];1105[label="wu3000",fontsize=16,color="green",shape="box"];1106[label="wu3000",fontsize=16,color="green",shape="box"];1101[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat wu61 wu62 == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="burlywood",shape="triangle"];2117[label="wu61/Succ wu610",fontsize=10,color="white",style="solid",shape="box"];1101 -> 2117[label="",style="solid", color="burlywood", weight=9];
2117 -> 1142[label="",style="solid", color="burlywood", weight=3];
2118[label="wu61/Zero",fontsize=10,color="white",style="solid",shape="box"];1101 -> 2118[label="",style="solid", color="burlywood", weight=9];
2118 -> 1143[label="",style="solid", color="burlywood", weight=3];
77[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (not False && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];77 -> 97[label="",style="solid", color="black", weight=3];
78[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (True && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];78 -> 98[label="",style="solid", color="black", weight=3];
79[label="index1 (Neg Zero) wu31 (Pos Zero) (True && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];79 -> 99[label="",style="solid", color="black", weight=3];
80[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) (not True && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];80 -> 100[label="",style="solid", color="black", weight=3];
81[label="index1 (Neg Zero) wu31 (Neg Zero) (True && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];81 -> 101[label="",style="solid", color="black", weight=3];
889[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat (Succ wu380) wu39 == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="burlywood",shape="box"];2119[label="wu39/Succ wu390",fontsize=10,color="white",style="solid",shape="box"];889 -> 2119[label="",style="solid", color="burlywood", weight=9];
2119 -> 932[label="",style="solid", color="burlywood", weight=3];
2120[label="wu39/Zero",fontsize=10,color="white",style="solid",shape="box"];889 -> 2120[label="",style="solid", color="burlywood", weight=9];
2120 -> 933[label="",style="solid", color="burlywood", weight=3];
890[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat Zero wu39 == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="burlywood",shape="box"];2121[label="wu39/Succ wu390",fontsize=10,color="white",style="solid",shape="box"];890 -> 2121[label="",style="solid", color="burlywood", weight=9];
2121 -> 934[label="",style="solid", color="burlywood", weight=3];
2122[label="wu39/Zero",fontsize=10,color="white",style="solid",shape="box"];890 -> 2122[label="",style="solid", color="burlywood", weight=9];
2122 -> 935[label="",style="solid", color="burlywood", weight=3];
86[label="index1 (Pos (Succ wu3000)) wu31 (Pos Zero) (False && Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];86 -> 106[label="",style="solid", color="black", weight=3];
87[label="index0 (Pos (Succ wu3000)) wu31 (Neg wu40) otherwise",fontsize=16,color="black",shape="box"];87 -> 107[label="",style="solid", color="black", weight=3];
88[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (True && Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];88 -> 108[label="",style="solid", color="black", weight=3];
89[label="index1 (Pos Zero) wu31 (Pos Zero) (Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];89 -> 109[label="",style="solid", color="black", weight=3];
90[label="index1 (Pos Zero) wu31 (Neg (Succ wu400)) False",fontsize=16,color="black",shape="box"];90 -> 110[label="",style="solid", color="black", weight=3];
91[label="index1 (Pos Zero) wu31 (Neg Zero) (Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];91 -> 111[label="",style="solid", color="black", weight=3];
92[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (compare (Pos wu40) wu31 /= GT)",fontsize=16,color="black",shape="box"];92 -> 112[label="",style="solid", color="black", weight=3];
1142[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat (Succ wu610) wu62 == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="burlywood",shape="box"];2123[label="wu62/Succ wu620",fontsize=10,color="white",style="solid",shape="box"];1142 -> 2123[label="",style="solid", color="burlywood", weight=9];
2123 -> 1174[label="",style="solid", color="burlywood", weight=3];
2124[label="wu62/Zero",fontsize=10,color="white",style="solid",shape="box"];1142 -> 2124[label="",style="solid", color="burlywood", weight=9];
2124 -> 1175[label="",style="solid", color="burlywood", weight=3];
1143[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat Zero wu62 == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="burlywood",shape="box"];2125[label="wu62/Succ wu620",fontsize=10,color="white",style="solid",shape="box"];1143 -> 2125[label="",style="solid", color="burlywood", weight=9];
2125 -> 1176[label="",style="solid", color="burlywood", weight=3];
2126[label="wu62/Zero",fontsize=10,color="white",style="solid",shape="box"];1143 -> 2126[label="",style="solid", color="burlywood", weight=9];
2126 -> 1177[label="",style="solid", color="burlywood", weight=3];
97[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (True && Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];97 -> 117[label="",style="solid", color="black", weight=3];
98[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];98 -> 118[label="",style="solid", color="black", weight=3];
99[label="index1 (Neg Zero) wu31 (Pos Zero) (Pos Zero <= wu31)",fontsize=16,color="black",shape="box"];99 -> 119[label="",style="solid", color="black", weight=3];
100[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) (False && Neg (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];100 -> 120[label="",style="solid", color="black", weight=3];
101[label="index1 (Neg Zero) wu31 (Neg Zero) (Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];101 -> 121[label="",style="solid", color="black", weight=3];
932[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat (Succ wu380) (Succ wu390) == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];932 -> 994[label="",style="solid", color="black", weight=3];
933[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat (Succ wu380) Zero == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];933 -> 995[label="",style="solid", color="black", weight=3];
934[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat Zero (Succ wu390) == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];934 -> 996[label="",style="solid", color="black", weight=3];
935[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat Zero Zero == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];935 -> 997[label="",style="solid", color="black", weight=3];
106[label="index1 (Pos (Succ wu3000)) wu31 (Pos Zero) False",fontsize=16,color="black",shape="box"];106 -> 127[label="",style="solid", color="black", weight=3];
107[label="index0 (Pos (Succ wu3000)) wu31 (Neg wu40) True",fontsize=16,color="black",shape="box"];107 -> 128[label="",style="solid", color="black", weight=3];
108[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (Pos (Succ wu400) <= wu31)",fontsize=16,color="black",shape="box"];108 -> 129[label="",style="solid", color="black", weight=3];
109[label="index1 (Pos Zero) wu31 (Pos Zero) (compare (Pos Zero) wu31 /= GT)",fontsize=16,color="black",shape="box"];109 -> 130[label="",style="solid", color="black", weight=3];
110[label="index0 (Pos Zero) wu31 (Neg (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];110 -> 131[label="",style="solid", color="black", weight=3];
111[label="index1 (Pos Zero) wu31 (Neg Zero) (compare (Neg Zero) wu31 /= GT)",fontsize=16,color="black",shape="box"];111 -> 132[label="",style="solid", color="black", weight=3];
112[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (not (compare (Pos wu40) wu31 == GT))",fontsize=16,color="black",shape="box"];112 -> 133[label="",style="solid", color="black", weight=3];
1174[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat (Succ wu610) (Succ wu620) == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1174 -> 1206[label="",style="solid", color="black", weight=3];
1175[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat (Succ wu610) Zero == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1175 -> 1207[label="",style="solid", color="black", weight=3];
1176[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat Zero (Succ wu620) == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1176 -> 1208[label="",style="solid", color="black", weight=3];
1177[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat Zero Zero == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1177 -> 1209[label="",style="solid", color="black", weight=3];
117[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (Neg Zero <= wu31)",fontsize=16,color="black",shape="box"];117 -> 139[label="",style="solid", color="black", weight=3];
118[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (compare (Pos (Succ wu400)) wu31 /= GT)",fontsize=16,color="black",shape="box"];118 -> 140[label="",style="solid", color="black", weight=3];
119[label="index1 (Neg Zero) wu31 (Pos Zero) (compare (Pos Zero) wu31 /= GT)",fontsize=16,color="black",shape="box"];119 -> 141[label="",style="solid", color="black", weight=3];
120[label="index1 (Neg Zero) wu31 (Neg (Succ wu400)) False",fontsize=16,color="black",shape="box"];120 -> 142[label="",style="solid", color="black", weight=3];
121[label="index1 (Neg Zero) wu31 (Neg Zero) (compare (Neg Zero) wu31 /= GT)",fontsize=16,color="black",shape="box"];121 -> 143[label="",style="solid", color="black", weight=3];
994 -> 853[label="",style="dashed", color="red", weight=0];
994[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpNat wu380 wu390 == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="magenta"];994 -> 1043[label="",style="dashed", color="magenta", weight=3];
994 -> 1044[label="",style="dashed", color="magenta", weight=3];
995[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (GT == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];995 -> 1045[label="",style="solid", color="black", weight=3];
996[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (LT == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];996 -> 1046[label="",style="solid", color="black", weight=3];
997[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (EQ == GT) && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];997 -> 1047[label="",style="solid", color="black", weight=3];
127[label="index0 (Pos (Succ wu3000)) wu31 (Pos Zero) otherwise",fontsize=16,color="black",shape="box"];127 -> 151[label="",style="solid", color="black", weight=3];
128[label="error []",fontsize=16,color="black",shape="triangle"];128 -> 152[label="",style="solid", color="black", weight=3];
129[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (compare (Pos (Succ wu400)) wu31 /= GT)",fontsize=16,color="black",shape="box"];129 -> 153[label="",style="solid", color="black", weight=3];
130[label="index1 (Pos Zero) wu31 (Pos Zero) (not (compare (Pos Zero) wu31 == GT))",fontsize=16,color="black",shape="box"];130 -> 154[label="",style="solid", color="black", weight=3];
131[label="index0 (Pos Zero) wu31 (Neg (Succ wu400)) True",fontsize=16,color="black",shape="box"];131 -> 155[label="",style="solid", color="black", weight=3];
132[label="index1 (Pos Zero) wu31 (Neg Zero) (not (compare (Neg Zero) wu31 == GT))",fontsize=16,color="black",shape="box"];132 -> 156[label="",style="solid", color="black", weight=3];
133[label="index1 (Neg (Succ wu3000)) wu31 (Pos wu40) (not (primCmpInt (Pos wu40) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2128[label="wu40/Succ wu400",fontsize=10,color="white",style="solid",shape="box"];133 -> 2128[label="",style="solid", color="burlywood", weight=9];
2128 -> 157[label="",style="solid", color="burlywood", weight=3];
2129[label="wu40/Zero",fontsize=10,color="white",style="solid",shape="box"];133 -> 2129[label="",style="solid", color="burlywood", weight=9];
2129 -> 158[label="",style="solid", color="burlywood", weight=3];
1206 -> 1101[label="",style="dashed", color="red", weight=0];
1206[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpNat wu610 wu620 == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="magenta"];1206 -> 1237[label="",style="dashed", color="magenta", weight=3];
1206 -> 1238[label="",style="dashed", color="magenta", weight=3];
1207[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (GT == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1207 -> 1239[label="",style="solid", color="black", weight=3];
1208[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (LT == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1208 -> 1240[label="",style="solid", color="black", weight=3];
1209[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (EQ == GT) && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1209 -> 1241[label="",style="solid", color="black", weight=3];
139[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (compare (Neg Zero) wu31 /= GT)",fontsize=16,color="black",shape="box"];139 -> 166[label="",style="solid", color="black", weight=3];
140[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (not (compare (Pos (Succ wu400)) wu31 == GT))",fontsize=16,color="black",shape="box"];140 -> 167[label="",style="solid", color="black", weight=3];
141[label="index1 (Neg Zero) wu31 (Pos Zero) (not (compare (Pos Zero) wu31 == GT))",fontsize=16,color="black",shape="box"];141 -> 168[label="",style="solid", color="black", weight=3];
142[label="index0 (Neg Zero) wu31 (Neg (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];142 -> 169[label="",style="solid", color="black", weight=3];
143[label="index1 (Neg Zero) wu31 (Neg Zero) (not (compare (Neg Zero) wu31 == GT))",fontsize=16,color="black",shape="box"];143 -> 170[label="",style="solid", color="black", weight=3];
1043[label="wu390",fontsize=16,color="green",shape="box"];1044[label="wu380",fontsize=16,color="green",shape="box"];1045[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not True && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];1045 -> 1063[label="",style="solid", color="black", weight=3];
1046[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not False && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="triangle"];1046 -> 1064[label="",style="solid", color="black", weight=3];
1047 -> 1046[label="",style="dashed", color="red", weight=0];
1047[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not False && Pos (Succ wu37) <= wu36)",fontsize=16,color="magenta"];151[label="index0 (Pos (Succ wu3000)) wu31 (Pos Zero) True",fontsize=16,color="black",shape="box"];151 -> 178[label="",style="solid", color="black", weight=3];
152[label="error []",fontsize=16,color="red",shape="box"];153[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not (compare (Pos (Succ wu400)) wu31 == GT))",fontsize=16,color="black",shape="box"];153 -> 179[label="",style="solid", color="black", weight=3];
154[label="index1 (Pos Zero) wu31 (Pos Zero) (not (primCmpInt (Pos Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2132[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];154 -> 2132[label="",style="solid", color="burlywood", weight=9];
2132 -> 180[label="",style="solid", color="burlywood", weight=3];
2133[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];154 -> 2133[label="",style="solid", color="burlywood", weight=9];
2133 -> 181[label="",style="solid", color="burlywood", weight=3];
155 -> 128[label="",style="dashed", color="red", weight=0];
155[label="error []",fontsize=16,color="magenta"];156[label="index1 (Pos Zero) wu31 (Neg Zero) (not (primCmpInt (Neg Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2135[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];156 -> 2135[label="",style="solid", color="burlywood", weight=9];
2135 -> 182[label="",style="solid", color="burlywood", weight=3];
2136[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];156 -> 2136[label="",style="solid", color="burlywood", weight=9];
2136 -> 183[label="",style="solid", color="burlywood", weight=3];
157[label="index1 (Neg (Succ wu3000)) wu31 (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2137[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];157 -> 2137[label="",style="solid", color="burlywood", weight=9];
2137 -> 184[label="",style="solid", color="burlywood", weight=3];
2138[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];157 -> 2138[label="",style="solid", color="burlywood", weight=9];
2138 -> 185[label="",style="solid", color="burlywood", weight=3];
158[label="index1 (Neg (Succ wu3000)) wu31 (Pos Zero) (not (primCmpInt (Pos Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2139[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];158 -> 2139[label="",style="solid", color="burlywood", weight=9];
2139 -> 186[label="",style="solid", color="burlywood", weight=3];
2140[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];158 -> 2140[label="",style="solid", color="burlywood", weight=9];
2140 -> 187[label="",style="solid", color="burlywood", weight=3];
1237[label="wu610",fontsize=16,color="green",shape="box"];1238[label="wu620",fontsize=16,color="green",shape="box"];1239[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not True && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1239 -> 1272[label="",style="solid", color="black", weight=3];
1240[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not False && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="triangle"];1240 -> 1273[label="",style="solid", color="black", weight=3];
1241 -> 1240[label="",style="dashed", color="red", weight=0];
1241[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not False && Neg (Succ wu60) <= wu59)",fontsize=16,color="magenta"];166[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (not (compare (Neg Zero) wu31 == GT))",fontsize=16,color="black",shape="box"];166 -> 195[label="",style="solid", color="black", weight=3];
167[label="index1 (Neg Zero) wu31 (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2142[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];167 -> 2142[label="",style="solid", color="burlywood", weight=9];
2142 -> 196[label="",style="solid", color="burlywood", weight=3];
2143[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];167 -> 2143[label="",style="solid", color="burlywood", weight=9];
2143 -> 197[label="",style="solid", color="burlywood", weight=3];
168[label="index1 (Neg Zero) wu31 (Pos Zero) (not (primCmpInt (Pos Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2144[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];168 -> 2144[label="",style="solid", color="burlywood", weight=9];
2144 -> 198[label="",style="solid", color="burlywood", weight=3];
2145[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];168 -> 2145[label="",style="solid", color="burlywood", weight=9];
2145 -> 199[label="",style="solid", color="burlywood", weight=3];
169[label="index0 (Neg Zero) wu31 (Neg (Succ wu400)) True",fontsize=16,color="black",shape="box"];169 -> 200[label="",style="solid", color="black", weight=3];
170[label="index1 (Neg Zero) wu31 (Neg Zero) (not (primCmpInt (Neg Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2146[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];170 -> 2146[label="",style="solid", color="burlywood", weight=9];
2146 -> 201[label="",style="solid", color="burlywood", weight=3];
2147[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];170 -> 2147[label="",style="solid", color="burlywood", weight=9];
2147 -> 202[label="",style="solid", color="burlywood", weight=3];
1063[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (False && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];1063 -> 1144[label="",style="solid", color="black", weight=3];
1064[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (True && Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];1064 -> 1145[label="",style="solid", color="black", weight=3];
178 -> 128[label="",style="dashed", color="red", weight=0];
178[label="error []",fontsize=16,color="magenta"];179[label="index1 (Pos Zero) wu31 (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2149[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];179 -> 2149[label="",style="solid", color="burlywood", weight=9];
2149 -> 211[label="",style="solid", color="burlywood", weight=3];
2150[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];179 -> 2150[label="",style="solid", color="burlywood", weight=9];
2150 -> 212[label="",style="solid", color="burlywood", weight=3];
180[label="index1 (Pos Zero) (Pos wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2151[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];180 -> 2151[label="",style="solid", color="burlywood", weight=9];
2151 -> 213[label="",style="solid", color="burlywood", weight=3];
2152[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];180 -> 2152[label="",style="solid", color="burlywood", weight=9];
2152 -> 214[label="",style="solid", color="burlywood", weight=3];
181[label="index1 (Pos Zero) (Neg wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2153[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];181 -> 2153[label="",style="solid", color="burlywood", weight=9];
2153 -> 215[label="",style="solid", color="burlywood", weight=3];
2154[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];181 -> 2154[label="",style="solid", color="burlywood", weight=9];
2154 -> 216[label="",style="solid", color="burlywood", weight=3];
182[label="index1 (Pos Zero) (Pos wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2155[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];182 -> 2155[label="",style="solid", color="burlywood", weight=9];
2155 -> 217[label="",style="solid", color="burlywood", weight=3];
2156[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];182 -> 2156[label="",style="solid", color="burlywood", weight=9];
2156 -> 218[label="",style="solid", color="burlywood", weight=3];
183[label="index1 (Pos Zero) (Neg wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2157[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];183 -> 2157[label="",style="solid", color="burlywood", weight=9];
2157 -> 219[label="",style="solid", color="burlywood", weight=3];
2158[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];183 -> 2158[label="",style="solid", color="burlywood", weight=9];
2158 -> 220[label="",style="solid", color="burlywood", weight=3];
184[label="index1 (Neg (Succ wu3000)) (Pos wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Pos wu310) == GT))",fontsize=16,color="black",shape="box"];184 -> 221[label="",style="solid", color="black", weight=3];
185[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Neg wu310) == GT))",fontsize=16,color="black",shape="box"];185 -> 222[label="",style="solid", color="black", weight=3];
186[label="index1 (Neg (Succ wu3000)) (Pos wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2159[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];186 -> 2159[label="",style="solid", color="burlywood", weight=9];
2159 -> 223[label="",style="solid", color="burlywood", weight=3];
2160[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];186 -> 2160[label="",style="solid", color="burlywood", weight=9];
2160 -> 224[label="",style="solid", color="burlywood", weight=3];
187[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2161[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];187 -> 2161[label="",style="solid", color="burlywood", weight=9];
2161 -> 225[label="",style="solid", color="burlywood", weight=3];
2162[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];187 -> 2162[label="",style="solid", color="burlywood", weight=9];
2162 -> 226[label="",style="solid", color="burlywood", weight=3];
1272[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (False && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1272 -> 1297[label="",style="solid", color="black", weight=3];
1273[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (True && Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1273 -> 1298[label="",style="solid", color="black", weight=3];
195[label="index1 (Neg (Succ wu3000)) wu31 (Neg Zero) (not (primCmpInt (Neg Zero) wu31 == GT))",fontsize=16,color="burlywood",shape="box"];2163[label="wu31/Pos wu310",fontsize=10,color="white",style="solid",shape="box"];195 -> 2163[label="",style="solid", color="burlywood", weight=9];
2163 -> 235[label="",style="solid", color="burlywood", weight=3];
2164[label="wu31/Neg wu310",fontsize=10,color="white",style="solid",shape="box"];195 -> 2164[label="",style="solid", color="burlywood", weight=9];
2164 -> 236[label="",style="solid", color="burlywood", weight=3];
196[label="index1 (Neg Zero) (Pos wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Pos wu310) == GT))",fontsize=16,color="black",shape="box"];196 -> 237[label="",style="solid", color="black", weight=3];
197[label="index1 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Neg wu310) == GT))",fontsize=16,color="black",shape="box"];197 -> 238[label="",style="solid", color="black", weight=3];
198[label="index1 (Neg Zero) (Pos wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2165[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];198 -> 2165[label="",style="solid", color="burlywood", weight=9];
2165 -> 239[label="",style="solid", color="burlywood", weight=3];
2166[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];198 -> 2166[label="",style="solid", color="burlywood", weight=9];
2166 -> 240[label="",style="solid", color="burlywood", weight=3];
199[label="index1 (Neg Zero) (Neg wu310) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2167[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];199 -> 2167[label="",style="solid", color="burlywood", weight=9];
2167 -> 241[label="",style="solid", color="burlywood", weight=3];
2168[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];199 -> 2168[label="",style="solid", color="burlywood", weight=9];
2168 -> 242[label="",style="solid", color="burlywood", weight=3];
200 -> 128[label="",style="dashed", color="red", weight=0];
200[label="error []",fontsize=16,color="magenta"];201[label="index1 (Neg Zero) (Pos wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2170[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];201 -> 2170[label="",style="solid", color="burlywood", weight=9];
2170 -> 243[label="",style="solid", color="burlywood", weight=3];
2171[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];201 -> 2171[label="",style="solid", color="burlywood", weight=9];
2171 -> 244[label="",style="solid", color="burlywood", weight=3];
202[label="index1 (Neg Zero) (Neg wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2172[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];202 -> 2172[label="",style="solid", color="burlywood", weight=9];
2172 -> 245[label="",style="solid", color="burlywood", weight=3];
2173[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];202 -> 2173[label="",style="solid", color="burlywood", weight=9];
2173 -> 246[label="",style="solid", color="burlywood", weight=3];
1144[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) False",fontsize=16,color="black",shape="triangle"];1144 -> 1178[label="",style="solid", color="black", weight=3];
1145[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (Pos (Succ wu37) <= wu36)",fontsize=16,color="black",shape="box"];1145 -> 1179[label="",style="solid", color="black", weight=3];
211[label="index1 (Pos Zero) (Pos wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Pos wu310) == GT))",fontsize=16,color="black",shape="box"];211 -> 257[label="",style="solid", color="black", weight=3];
212[label="index1 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) (not (primCmpInt (Pos (Succ wu400)) (Neg wu310) == GT))",fontsize=16,color="black",shape="box"];212 -> 258[label="",style="solid", color="black", weight=3];
213[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];213 -> 259[label="",style="solid", color="black", weight=3];
214[label="index1 (Pos Zero) (Pos Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];214 -> 260[label="",style="solid", color="black", weight=3];
215[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];215 -> 261[label="",style="solid", color="black", weight=3];
216[label="index1 (Pos Zero) (Neg Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];216 -> 262[label="",style="solid", color="black", weight=3];
217[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];217 -> 263[label="",style="solid", color="black", weight=3];
218[label="index1 (Pos Zero) (Pos Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];218 -> 264[label="",style="solid", color="black", weight=3];
219[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];219 -> 265[label="",style="solid", color="black", weight=3];
220[label="index1 (Pos Zero) (Neg Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];220 -> 266[label="",style="solid", color="black", weight=3];
221[label="index1 (Neg (Succ wu3000)) (Pos wu310) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) wu310 == GT))",fontsize=16,color="burlywood",shape="box"];2174[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];221 -> 2174[label="",style="solid", color="burlywood", weight=9];
2174 -> 267[label="",style="solid", color="burlywood", weight=3];
2175[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];221 -> 2175[label="",style="solid", color="burlywood", weight=9];
2175 -> 268[label="",style="solid", color="burlywood", weight=3];
222[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];222 -> 269[label="",style="solid", color="black", weight=3];
223[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];223 -> 270[label="",style="solid", color="black", weight=3];
224[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];224 -> 271[label="",style="solid", color="black", weight=3];
225[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];225 -> 272[label="",style="solid", color="black", weight=3];
226[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];226 -> 273[label="",style="solid", color="black", weight=3];
1297[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) False",fontsize=16,color="black",shape="triangle"];1297 -> 1304[label="",style="solid", color="black", weight=3];
1298[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (Neg (Succ wu60) <= wu59)",fontsize=16,color="black",shape="box"];1298 -> 1305[label="",style="solid", color="black", weight=3];
235[label="index1 (Neg (Succ wu3000)) (Pos wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2176[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];235 -> 2176[label="",style="solid", color="burlywood", weight=9];
2176 -> 284[label="",style="solid", color="burlywood", weight=3];
2177[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];235 -> 2177[label="",style="solid", color="burlywood", weight=9];
2177 -> 285[label="",style="solid", color="burlywood", weight=3];
236[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg wu310) == GT))",fontsize=16,color="burlywood",shape="box"];2178[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];236 -> 2178[label="",style="solid", color="burlywood", weight=9];
2178 -> 286[label="",style="solid", color="burlywood", weight=3];
2179[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];236 -> 2179[label="",style="solid", color="burlywood", weight=9];
2179 -> 287[label="",style="solid", color="burlywood", weight=3];
237[label="index1 (Neg Zero) (Pos wu310) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) wu310 == GT))",fontsize=16,color="burlywood",shape="box"];2180[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];237 -> 2180[label="",style="solid", color="burlywood", weight=9];
2180 -> 288[label="",style="solid", color="burlywood", weight=3];
2181[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];237 -> 2181[label="",style="solid", color="burlywood", weight=9];
2181 -> 289[label="",style="solid", color="burlywood", weight=3];
238[label="index1 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];238 -> 290[label="",style="solid", color="black", weight=3];
239[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];239 -> 291[label="",style="solid", color="black", weight=3];
240[label="index1 (Neg Zero) (Pos Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];240 -> 292[label="",style="solid", color="black", weight=3];
241[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];241 -> 293[label="",style="solid", color="black", weight=3];
242[label="index1 (Neg Zero) (Neg Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];242 -> 294[label="",style="solid", color="black", weight=3];
243[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];243 -> 295[label="",style="solid", color="black", weight=3];
244[label="index1 (Neg Zero) (Pos Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];244 -> 296[label="",style="solid", color="black", weight=3];
245[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];245 -> 297[label="",style="solid", color="black", weight=3];
246[label="index1 (Neg Zero) (Neg Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];246 -> 298[label="",style="solid", color="black", weight=3];
1178[label="index0 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) otherwise",fontsize=16,color="black",shape="box"];1178 -> 1210[label="",style="solid", color="black", weight=3];
1179[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (compare (Pos (Succ wu37)) wu36 /= GT)",fontsize=16,color="black",shape="box"];1179 -> 1211[label="",style="solid", color="black", weight=3];
257[label="index1 (Pos Zero) (Pos wu310) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) wu310 == GT))",fontsize=16,color="burlywood",shape="box"];2182[label="wu310/Succ wu3100",fontsize=10,color="white",style="solid",shape="box"];257 -> 2182[label="",style="solid", color="burlywood", weight=9];
2182 -> 309[label="",style="solid", color="burlywood", weight=3];
2183[label="wu310/Zero",fontsize=10,color="white",style="solid",shape="box"];257 -> 2183[label="",style="solid", color="burlywood", weight=9];
2183 -> 310[label="",style="solid", color="burlywood", weight=3];
258[label="index1 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];258 -> 311[label="",style="solid", color="black", weight=3];
259[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpNat Zero (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];259 -> 312[label="",style="solid", color="black", weight=3];
260[label="index1 (Pos Zero) (Pos Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];260 -> 313[label="",style="solid", color="black", weight=3];
261[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];261 -> 314[label="",style="solid", color="black", weight=3];
262[label="index1 (Pos Zero) (Neg Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];262 -> 315[label="",style="solid", color="black", weight=3];
263[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Neg Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];263 -> 316[label="",style="solid", color="black", weight=3];
264[label="index1 (Pos Zero) (Pos Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];264 -> 317[label="",style="solid", color="black", weight=3];
265[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpNat (Succ wu3100) Zero == GT))",fontsize=16,color="black",shape="box"];265 -> 318[label="",style="solid", color="black", weight=3];
266[label="index1 (Pos Zero) (Neg Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];266 -> 319[label="",style="solid", color="black", weight=3];
267[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];267 -> 320[label="",style="solid", color="black", weight=3];
268[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) Zero == GT))",fontsize=16,color="black",shape="box"];268 -> 321[label="",style="solid", color="black", weight=3];
269[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];269 -> 322[label="",style="solid", color="black", weight=3];
270[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpNat Zero (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];270 -> 323[label="",style="solid", color="black", weight=3];
271[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];271 -> 324[label="",style="solid", color="black", weight=3];
272[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];272 -> 325[label="",style="solid", color="black", weight=3];
273[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];273 -> 326[label="",style="solid", color="black", weight=3];
1304[label="index0 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) otherwise",fontsize=16,color="black",shape="box"];1304 -> 1312[label="",style="solid", color="black", weight=3];
1305[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (compare (Neg (Succ wu60)) wu59 /= GT)",fontsize=16,color="black",shape="box"];1305 -> 1313[label="",style="solid", color="black", weight=3];
284[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];284 -> 337[label="",style="solid", color="black", weight=3];
285[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];285 -> 338[label="",style="solid", color="black", weight=3];
286[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg (Succ wu3100)) == GT))",fontsize=16,color="black",shape="box"];286 -> 339[label="",style="solid", color="black", weight=3];
287[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Neg Zero) (not (primCmpInt (Neg Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];287 -> 340[label="",style="solid", color="black", weight=3];
288[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];288 -> 341[label="",style="solid", color="black", weight=3];
289[label="index1 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) Zero == GT))",fontsize=16,color="black",shape="box"];289 -> 342[label="",style="solid", color="black", weight=3];
290[label="index1 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];290 -> 343[label="",style="solid", color="black", weight=3];
291[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos Zero) (not (primCmpNat Zero (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];291 -> 344[label="",style="solid", color="black", weight=3];
292[label="index1 (Neg Zero) (Pos Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];292 -> 345[label="",style="solid", color="black", weight=3];
293[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];293 -> 346[label="",style="solid", color="black", weight=3];
294[label="index1 (Neg Zero) (Neg Zero) (Pos Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];294 -> 347[label="",style="solid", color="black", weight=3];
295[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Neg Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];295 -> 348[label="",style="solid", color="black", weight=3];
296[label="index1 (Neg Zero) (Pos Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];296 -> 349[label="",style="solid", color="black", weight=3];
297[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpNat (Succ wu3100) Zero == GT))",fontsize=16,color="black",shape="box"];297 -> 350[label="",style="solid", color="black", weight=3];
298[label="index1 (Neg Zero) (Neg Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];298 -> 351[label="",style="solid", color="black", weight=3];
1210[label="index0 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) True",fontsize=16,color="black",shape="box"];1210 -> 1242[label="",style="solid", color="black", weight=3];
1211[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (compare (Pos (Succ wu37)) wu36 == GT))",fontsize=16,color="black",shape="box"];1211 -> 1243[label="",style="solid", color="black", weight=3];
309[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) (Succ wu3100) == GT))",fontsize=16,color="black",shape="box"];309 -> 364[label="",style="solid", color="black", weight=3];
310[label="index1 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) (not (primCmpNat (Succ wu400) Zero == GT))",fontsize=16,color="black",shape="box"];310 -> 365[label="",style="solid", color="black", weight=3];
311[label="index1 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];311 -> 366[label="",style="solid", color="black", weight=3];
312[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];312 -> 367[label="",style="solid", color="black", weight=3];
313[label="index1 (Pos Zero) (Pos Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];313 -> 368[label="",style="solid", color="black", weight=3];
314[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) (not True)",fontsize=16,color="black",shape="box"];314 -> 369[label="",style="solid", color="black", weight=3];
315[label="index1 (Pos Zero) (Neg Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];315 -> 370[label="",style="solid", color="black", weight=3];
316[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];316 -> 371[label="",style="solid", color="black", weight=3];
317[label="index1 (Pos Zero) (Pos Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];317 -> 372[label="",style="solid", color="black", weight=3];
318[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];318 -> 373[label="",style="solid", color="black", weight=3];
319[label="index1 (Pos Zero) (Neg Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];319 -> 374[label="",style="solid", color="black", weight=3];
320 -> 1407[label="",style="dashed", color="red", weight=0];
320[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat wu400 wu3100 == GT))",fontsize=16,color="magenta"];320 -> 1408[label="",style="dashed", color="magenta", weight=3];
320 -> 1409[label="",style="dashed", color="magenta", weight=3];
320 -> 1410[label="",style="dashed", color="magenta", weight=3];
320 -> 1411[label="",style="dashed", color="magenta", weight=3];
320 -> 1412[label="",style="dashed", color="magenta", weight=3];
321[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];321 -> 377[label="",style="solid", color="black", weight=3];
322[label="index1 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];322 -> 378[label="",style="solid", color="black", weight=3];
323[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];323 -> 379[label="",style="solid", color="black", weight=3];
324[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];324 -> 380[label="",style="solid", color="black", weight=3];
325[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) (not True)",fontsize=16,color="black",shape="box"];325 -> 381[label="",style="solid", color="black", weight=3];
326[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];326 -> 382[label="",style="solid", color="black", weight=3];
1312[label="index0 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) True",fontsize=16,color="black",shape="box"];1312 -> 1327[label="",style="solid", color="black", weight=3];
1313[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (compare (Neg (Succ wu60)) wu59 == GT))",fontsize=16,color="black",shape="box"];1313 -> 1328[label="",style="solid", color="black", weight=3];
337[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Neg Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];337 -> 395[label="",style="solid", color="black", weight=3];
338[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];338 -> 396[label="",style="solid", color="black", weight=3];
339[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) (not (primCmpNat (Succ wu3100) Zero == GT))",fontsize=16,color="black",shape="box"];339 -> 397[label="",style="solid", color="black", weight=3];
340[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Neg Zero) (not (EQ == GT))",fontsize=16,color="black",shape="box"];340 -> 398[label="",style="solid", color="black", weight=3];
341 -> 1617[label="",style="dashed", color="red", weight=0];
341[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat wu400 wu3100 == GT))",fontsize=16,color="magenta"];341 -> 1618[label="",style="dashed", color="magenta", weight=3];
341 -> 1619[label="",style="dashed", color="magenta", weight=3];
341 -> 1620[label="",style="dashed", color="magenta", weight=3];
341 -> 1621[label="",style="dashed", color="magenta", weight=3];
342[label="index1 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];342 -> 401[label="",style="solid", color="black", weight=3];
343[label="index1 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];343 -> 402[label="",style="solid", color="black", weight=3];
344[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];344 -> 403[label="",style="solid", color="black", weight=3];
345[label="index1 (Neg Zero) (Pos Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];345 -> 404[label="",style="solid", color="black", weight=3];
346[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) (not True)",fontsize=16,color="black",shape="box"];346 -> 405[label="",style="solid", color="black", weight=3];
347[label="index1 (Neg Zero) (Neg Zero) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];347 -> 406[label="",style="solid", color="black", weight=3];
348[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];348 -> 407[label="",style="solid", color="black", weight=3];
349[label="index1 (Neg Zero) (Pos Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];349 -> 408[label="",style="solid", color="black", weight=3];
350[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];350 -> 409[label="",style="solid", color="black", weight=3];
351[label="index1 (Neg Zero) (Neg Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];351 -> 410[label="",style="solid", color="black", weight=3];
1242 -> 128[label="",style="dashed", color="red", weight=0];
1242[label="error []",fontsize=16,color="magenta"];1243[label="index1 (Pos (Succ wu35)) wu36 (Pos (Succ wu37)) (not (primCmpInt (Pos (Succ wu37)) wu36 == GT))",fontsize=16,color="burlywood",shape="box"];2187[label="wu36/Pos wu360",fontsize=10,color="white",style="solid",shape="box"];1243 -> 2187[label="",style="solid", color="burlywood", weight=9];
2187 -> 1274[label="",style="solid", color="burlywood", weight=3];
2188[label="wu36/Neg wu360",fontsize=10,color="white",style="solid",shape="box"];1243 -> 2188[label="",style="solid", color="burlywood", weight=9];
2188 -> 1275[label="",style="solid", color="burlywood", weight=3];
364 -> 1494[label="",style="dashed", color="red", weight=0];
364[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos (Succ wu400)) (not (primCmpNat wu400 wu3100 == GT))",fontsize=16,color="magenta"];364 -> 1495[label="",style="dashed", color="magenta", weight=3];
364 -> 1496[label="",style="dashed", color="magenta", weight=3];
364 -> 1497[label="",style="dashed", color="magenta", weight=3];
364 -> 1498[label="",style="dashed", color="magenta", weight=3];
365[label="index1 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) (not (GT == GT))",fontsize=16,color="black",shape="box"];365 -> 427[label="",style="solid", color="black", weight=3];
366[label="index1 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];366 -> 428[label="",style="solid", color="black", weight=3];
367[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];367 -> 429[label="",style="solid", color="black", weight=3];
368[label="index1 (Pos Zero) (Pos Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];368 -> 430[label="",style="solid", color="black", weight=3];
369[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) False",fontsize=16,color="black",shape="box"];369 -> 431[label="",style="solid", color="black", weight=3];
370[label="index1 (Pos Zero) (Neg Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];370 -> 432[label="",style="solid", color="black", weight=3];
371[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];371 -> 433[label="",style="solid", color="black", weight=3];
372[label="index1 (Pos Zero) (Pos Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];372 -> 434[label="",style="solid", color="black", weight=3];
373[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) (not True)",fontsize=16,color="black",shape="box"];373 -> 435[label="",style="solid", color="black", weight=3];
374[label="index1 (Pos Zero) (Neg Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];374 -> 436[label="",style="solid", color="black", weight=3];
1408[label="wu400",fontsize=16,color="green",shape="box"];1409[label="wu3000",fontsize=16,color="green",shape="box"];1410[label="wu3100",fontsize=16,color="green",shape="box"];1411[label="wu3100",fontsize=16,color="green",shape="box"];1412[label="wu400",fontsize=16,color="green",shape="box"];1407[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat wu99 wu100 == GT))",fontsize=16,color="burlywood",shape="triangle"];2190[label="wu99/Succ wu990",fontsize=10,color="white",style="solid",shape="box"];1407 -> 2190[label="",style="solid", color="burlywood", weight=9];
2190 -> 1443[label="",style="solid", color="burlywood", weight=3];
2191[label="wu99/Zero",fontsize=10,color="white",style="solid",shape="box"];1407 -> 2191[label="",style="solid", color="burlywood", weight=9];
2191 -> 1444[label="",style="solid", color="burlywood", weight=3];
377[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];377 -> 441[label="",style="solid", color="black", weight=3];
378[label="index0 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];378 -> 442[label="",style="solid", color="black", weight=3];
379[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];379 -> 443[label="",style="solid", color="black", weight=3];
380[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];380 -> 444[label="",style="solid", color="black", weight=3];
381[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) False",fontsize=16,color="black",shape="box"];381 -> 445[label="",style="solid", color="black", weight=3];
382[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];382 -> 446[label="",style="solid", color="black", weight=3];
1327 -> 128[label="",style="dashed", color="red", weight=0];
1327[label="error []",fontsize=16,color="magenta"];1328[label="index1 (Neg (Succ wu58)) wu59 (Neg (Succ wu60)) (not (primCmpInt (Neg (Succ wu60)) wu59 == GT))",fontsize=16,color="burlywood",shape="box"];2193[label="wu59/Pos wu590",fontsize=10,color="white",style="solid",shape="box"];1328 -> 2193[label="",style="solid", color="burlywood", weight=9];
2193 -> 1335[label="",style="solid", color="burlywood", weight=3];
2194[label="wu59/Neg wu590",fontsize=10,color="white",style="solid",shape="box"];1328 -> 2194[label="",style="solid", color="burlywood", weight=9];
2194 -> 1336[label="",style="solid", color="burlywood", weight=3];
395[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];395 -> 461[label="",style="solid", color="black", weight=3];
396[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];396 -> 462[label="",style="solid", color="black", weight=3];
397[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) (not (GT == GT))",fontsize=16,color="black",shape="box"];397 -> 463[label="",style="solid", color="black", weight=3];
398[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];398 -> 464[label="",style="solid", color="black", weight=3];
1618[label="wu400",fontsize=16,color="green",shape="box"];1619[label="wu3100",fontsize=16,color="green",shape="box"];1620[label="wu3100",fontsize=16,color="green",shape="box"];1621[label="wu400",fontsize=16,color="green",shape="box"];1617[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat wu112 wu113 == GT))",fontsize=16,color="burlywood",shape="triangle"];2195[label="wu112/Succ wu1120",fontsize=10,color="white",style="solid",shape="box"];1617 -> 2195[label="",style="solid", color="burlywood", weight=9];
2195 -> 1650[label="",style="solid", color="burlywood", weight=3];
2196[label="wu112/Zero",fontsize=10,color="white",style="solid",shape="box"];1617 -> 2196[label="",style="solid", color="burlywood", weight=9];
2196 -> 1651[label="",style="solid", color="burlywood", weight=3];
401[label="index1 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];401 -> 469[label="",style="solid", color="black", weight=3];
402[label="index0 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];402 -> 470[label="",style="solid", color="black", weight=3];
403[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];403 -> 471[label="",style="solid", color="black", weight=3];
404[label="index1 (Neg Zero) (Pos Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];404 -> 472[label="",style="solid", color="black", weight=3];
405[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) False",fontsize=16,color="black",shape="box"];405 -> 473[label="",style="solid", color="black", weight=3];
406[label="index1 (Neg Zero) (Neg Zero) (Pos Zero) True",fontsize=16,color="black",shape="box"];406 -> 474[label="",style="solid", color="black", weight=3];
407[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];407 -> 475[label="",style="solid", color="black", weight=3];
408[label="index1 (Neg Zero) (Pos Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];408 -> 476[label="",style="solid", color="black", weight=3];
409[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) (not True)",fontsize=16,color="black",shape="box"];409 -> 477[label="",style="solid", color="black", weight=3];
410[label="index1 (Neg Zero) (Neg Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];410 -> 478[label="",style="solid", color="black", weight=3];
1274[label="index1 (Pos (Succ wu35)) (Pos wu360) (Pos (Succ wu37)) (not (primCmpInt (Pos (Succ wu37)) (Pos wu360) == GT))",fontsize=16,color="black",shape="box"];1274 -> 1299[label="",style="solid", color="black", weight=3];
1275[label="index1 (Pos (Succ wu35)) (Neg wu360) (Pos (Succ wu37)) (not (primCmpInt (Pos (Succ wu37)) (Neg wu360) == GT))",fontsize=16,color="black",shape="box"];1275 -> 1300[label="",style="solid", color="black", weight=3];
1495[label="wu3100",fontsize=16,color="green",shape="box"];1496[label="wu3100",fontsize=16,color="green",shape="box"];1497[label="wu400",fontsize=16,color="green",shape="box"];1498[label="wu400",fontsize=16,color="green",shape="box"];1494[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat wu107 wu108 == GT))",fontsize=16,color="burlywood",shape="triangle"];2197[label="wu107/Succ wu1070",fontsize=10,color="white",style="solid",shape="box"];1494 -> 2197[label="",style="solid", color="burlywood", weight=9];
2197 -> 1523[label="",style="solid", color="burlywood", weight=3];
2198[label="wu107/Zero",fontsize=10,color="white",style="solid",shape="box"];1494 -> 2198[label="",style="solid", color="burlywood", weight=9];
2198 -> 1524[label="",style="solid", color="burlywood", weight=3];
427[label="index1 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) (not True)",fontsize=16,color="black",shape="box"];427 -> 499[label="",style="solid", color="black", weight=3];
428[label="index0 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];428 -> 500[label="",style="solid", color="black", weight=3];
429[label="index1 (Pos Zero) (Pos (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];429 -> 501[label="",style="solid", color="black", weight=3];
430[label="Pos Zero - Pos Zero",fontsize=16,color="black",shape="triangle"];430 -> 502[label="",style="solid", color="black", weight=3];
431[label="index0 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) otherwise",fontsize=16,color="black",shape="box"];431 -> 503[label="",style="solid", color="black", weight=3];
432 -> 430[label="",style="dashed", color="red", weight=0];
432[label="Pos Zero - Pos Zero",fontsize=16,color="magenta"];433[label="Neg Zero - Pos Zero",fontsize=16,color="black",shape="triangle"];433 -> 504[label="",style="solid", color="black", weight=3];
434 -> 433[label="",style="dashed", color="red", weight=0];
434[label="Neg Zero - Pos Zero",fontsize=16,color="magenta"];435[label="index1 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) False",fontsize=16,color="black",shape="box"];435 -> 505[label="",style="solid", color="black", weight=3];
436 -> 433[label="",style="dashed", color="red", weight=0];
436[label="Neg Zero - Pos Zero",fontsize=16,color="magenta"];1443[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat (Succ wu990) wu100 == GT))",fontsize=16,color="burlywood",shape="box"];2202[label="wu100/Succ wu1000",fontsize=10,color="white",style="solid",shape="box"];1443 -> 2202[label="",style="solid", color="burlywood", weight=9];
2202 -> 1473[label="",style="solid", color="burlywood", weight=3];
2203[label="wu100/Zero",fontsize=10,color="white",style="solid",shape="box"];1443 -> 2203[label="",style="solid", color="burlywood", weight=9];
2203 -> 1474[label="",style="solid", color="burlywood", weight=3];
1444[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat Zero wu100 == GT))",fontsize=16,color="burlywood",shape="box"];2204[label="wu100/Succ wu1000",fontsize=10,color="white",style="solid",shape="box"];1444 -> 2204[label="",style="solid", color="burlywood", weight=9];
2204 -> 1475[label="",style="solid", color="burlywood", weight=3];
2205[label="wu100/Zero",fontsize=10,color="white",style="solid",shape="box"];1444 -> 2205[label="",style="solid", color="burlywood", weight=9];
2205 -> 1476[label="",style="solid", color="burlywood", weight=3];
441[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];441 -> 510[label="",style="solid", color="black", weight=3];
442[label="index0 (Neg (Succ wu3000)) (Neg wu310) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];442 -> 511[label="",style="solid", color="black", weight=3];
443[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];443 -> 512[label="",style="solid", color="black", weight=3];
444[label="Pos Zero - Neg (Succ wu3000)",fontsize=16,color="black",shape="triangle"];444 -> 513[label="",style="solid", color="black", weight=3];
445[label="index0 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) otherwise",fontsize=16,color="black",shape="box"];445 -> 514[label="",style="solid", color="black", weight=3];
446 -> 444[label="",style="dashed", color="red", weight=0];
446[label="Pos Zero - Neg (Succ wu3000)",fontsize=16,color="magenta"];1335[label="index1 (Neg (Succ wu58)) (Pos wu590) (Neg (Succ wu60)) (not (primCmpInt (Neg (Succ wu60)) (Pos wu590) == GT))",fontsize=16,color="black",shape="box"];1335 -> 1344[label="",style="solid", color="black", weight=3];
1336[label="index1 (Neg (Succ wu58)) (Neg wu590) (Neg (Succ wu60)) (not (primCmpInt (Neg (Succ wu60)) (Neg wu590) == GT))",fontsize=16,color="black",shape="box"];1336 -> 1345[label="",style="solid", color="black", weight=3];
461[label="index1 (Neg (Succ wu3000)) (Pos (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];461 -> 531[label="",style="solid", color="black", weight=3];
462[label="index1 (Neg (Succ wu3000)) (Pos Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];462 -> 532[label="",style="solid", color="black", weight=3];
463[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) (not True)",fontsize=16,color="black",shape="box"];463 -> 533[label="",style="solid", color="black", weight=3];
464[label="index1 (Neg (Succ wu3000)) (Neg Zero) (Neg Zero) True",fontsize=16,color="black",shape="box"];464 -> 534[label="",style="solid", color="black", weight=3];
1650[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat (Succ wu1120) wu113 == GT))",fontsize=16,color="burlywood",shape="box"];2207[label="wu113/Succ wu1130",fontsize=10,color="white",style="solid",shape="box"];1650 -> 2207[label="",style="solid", color="burlywood", weight=9];
2207 -> 1677[label="",style="solid", color="burlywood", weight=3];
2208[label="wu113/Zero",fontsize=10,color="white",style="solid",shape="box"];1650 -> 2208[label="",style="solid", color="burlywood", weight=9];
2208 -> 1678[label="",style="solid", color="burlywood", weight=3];
1651[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat Zero wu113 == GT))",fontsize=16,color="burlywood",shape="box"];2209[label="wu113/Succ wu1130",fontsize=10,color="white",style="solid",shape="box"];1651 -> 2209[label="",style="solid", color="burlywood", weight=9];
2209 -> 1679[label="",style="solid", color="burlywood", weight=3];
2210[label="wu113/Zero",fontsize=10,color="white",style="solid",shape="box"];1651 -> 2210[label="",style="solid", color="burlywood", weight=9];
2210 -> 1680[label="",style="solid", color="burlywood", weight=3];
469[label="index1 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];469 -> 539[label="",style="solid", color="black", weight=3];
470[label="index0 (Neg Zero) (Neg wu310) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];470 -> 540[label="",style="solid", color="black", weight=3];
471[label="index1 (Neg Zero) (Pos (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];471 -> 541[label="",style="solid", color="black", weight=3];
472[label="Pos Zero - Neg Zero",fontsize=16,color="black",shape="triangle"];472 -> 542[label="",style="solid", color="black", weight=3];
473[label="index0 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) otherwise",fontsize=16,color="black",shape="box"];473 -> 543[label="",style="solid", color="black", weight=3];
474 -> 472[label="",style="dashed", color="red", weight=0];
474[label="Pos Zero - Neg Zero",fontsize=16,color="magenta"];475[label="Neg Zero - Neg Zero",fontsize=16,color="black",shape="triangle"];475 -> 544[label="",style="solid", color="black", weight=3];
476 -> 475[label="",style="dashed", color="red", weight=0];
476[label="Neg Zero - Neg Zero",fontsize=16,color="magenta"];477[label="index1 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) False",fontsize=16,color="black",shape="box"];477 -> 545[label="",style="solid", color="black", weight=3];
478 -> 475[label="",style="dashed", color="red", weight=0];
478[label="Neg Zero - Neg Zero",fontsize=16,color="magenta"];1299[label="index1 (Pos (Succ wu35)) (Pos wu360) (Pos (Succ wu37)) (not (primCmpNat (Succ wu37) wu360 == GT))",fontsize=16,color="burlywood",shape="box"];2214[label="wu360/Succ wu3600",fontsize=10,color="white",style="solid",shape="box"];1299 -> 2214[label="",style="solid", color="burlywood", weight=9];
2214 -> 1306[label="",style="solid", color="burlywood", weight=3];
2215[label="wu360/Zero",fontsize=10,color="white",style="solid",shape="box"];1299 -> 2215[label="",style="solid", color="burlywood", weight=9];
2215 -> 1307[label="",style="solid", color="burlywood", weight=3];
1300[label="index1 (Pos (Succ wu35)) (Neg wu360) (Pos (Succ wu37)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1300 -> 1308[label="",style="solid", color="black", weight=3];
1523[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat (Succ wu1070) wu108 == GT))",fontsize=16,color="burlywood",shape="box"];2216[label="wu108/Succ wu1080",fontsize=10,color="white",style="solid",shape="box"];1523 -> 2216[label="",style="solid", color="burlywood", weight=9];
2216 -> 1557[label="",style="solid", color="burlywood", weight=3];
2217[label="wu108/Zero",fontsize=10,color="white",style="solid",shape="box"];1523 -> 2217[label="",style="solid", color="burlywood", weight=9];
2217 -> 1558[label="",style="solid", color="burlywood", weight=3];
1524[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat Zero wu108 == GT))",fontsize=16,color="burlywood",shape="box"];2218[label="wu108/Succ wu1080",fontsize=10,color="white",style="solid",shape="box"];1524 -> 2218[label="",style="solid", color="burlywood", weight=9];
2218 -> 1559[label="",style="solid", color="burlywood", weight=3];
2219[label="wu108/Zero",fontsize=10,color="white",style="solid",shape="box"];1524 -> 2219[label="",style="solid", color="burlywood", weight=9];
2219 -> 1560[label="",style="solid", color="burlywood", weight=3];
499[label="index1 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) False",fontsize=16,color="black",shape="box"];499 -> 568[label="",style="solid", color="black", weight=3];
500[label="index0 (Pos Zero) (Neg wu310) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];500 -> 569[label="",style="solid", color="black", weight=3];
501 -> 430[label="",style="dashed", color="red", weight=0];
501[label="Pos Zero - Pos Zero",fontsize=16,color="magenta"];502[label="primMinusInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];502 -> 570[label="",style="solid", color="black", weight=3];
503[label="index0 (Pos Zero) (Neg (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];503 -> 571[label="",style="solid", color="black", weight=3];
504[label="primMinusInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];504 -> 572[label="",style="solid", color="black", weight=3];
505[label="index0 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) otherwise",fontsize=16,color="black",shape="box"];505 -> 573[label="",style="solid", color="black", weight=3];
1473[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat (Succ wu990) (Succ wu1000) == GT))",fontsize=16,color="black",shape="box"];1473 -> 1525[label="",style="solid", color="black", weight=3];
1474[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat (Succ wu990) Zero == GT))",fontsize=16,color="black",shape="box"];1474 -> 1526[label="",style="solid", color="black", weight=3];
1475[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat Zero (Succ wu1000) == GT))",fontsize=16,color="black",shape="box"];1475 -> 1527[label="",style="solid", color="black", weight=3];
1476[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1476 -> 1528[label="",style="solid", color="black", weight=3];
510[label="index0 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];510 -> 579[label="",style="solid", color="black", weight=3];
511 -> 128[label="",style="dashed", color="red", weight=0];
511[label="error []",fontsize=16,color="magenta"];512 -> 444[label="",style="dashed", color="red", weight=0];
512[label="Pos Zero - Neg (Succ wu3000)",fontsize=16,color="magenta"];513[label="primMinusInt (Pos Zero) (Neg (Succ wu3000))",fontsize=16,color="black",shape="box"];513 -> 580[label="",style="solid", color="black", weight=3];
514[label="index0 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];514 -> 581[label="",style="solid", color="black", weight=3];
1344[label="index1 (Neg (Succ wu58)) (Pos wu590) (Neg (Succ wu60)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1344 -> 1359[label="",style="solid", color="black", weight=3];
1345[label="index1 (Neg (Succ wu58)) (Neg wu590) (Neg (Succ wu60)) (not (primCmpNat wu590 (Succ wu60) == GT))",fontsize=16,color="burlywood",shape="box"];2223[label="wu590/Succ wu5900",fontsize=10,color="white",style="solid",shape="box"];1345 -> 2223[label="",style="solid", color="burlywood", weight=9];
2223 -> 1360[label="",style="solid", color="burlywood", weight=3];
2224[label="wu590/Zero",fontsize=10,color="white",style="solid",shape="box"];1345 -> 2224[label="",style="solid", color="burlywood", weight=9];
2224 -> 1361[label="",style="solid", color="burlywood", weight=3];
531[label="Neg Zero - Neg (Succ wu3000)",fontsize=16,color="black",shape="triangle"];531 -> 600[label="",style="solid", color="black", weight=3];
532 -> 531[label="",style="dashed", color="red", weight=0];
532[label="Neg Zero - Neg (Succ wu3000)",fontsize=16,color="magenta"];533[label="index1 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) False",fontsize=16,color="black",shape="box"];533 -> 601[label="",style="solid", color="black", weight=3];
534 -> 531[label="",style="dashed", color="red", weight=0];
534[label="Neg Zero - Neg (Succ wu3000)",fontsize=16,color="magenta"];1677[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat (Succ wu1120) (Succ wu1130) == GT))",fontsize=16,color="black",shape="box"];1677 -> 1698[label="",style="solid", color="black", weight=3];
1678[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat (Succ wu1120) Zero == GT))",fontsize=16,color="black",shape="box"];1678 -> 1699[label="",style="solid", color="black", weight=3];
1679[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat Zero (Succ wu1130) == GT))",fontsize=16,color="black",shape="box"];1679 -> 1700[label="",style="solid", color="black", weight=3];
1680[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1680 -> 1701[label="",style="solid", color="black", weight=3];
539[label="index0 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];539 -> 607[label="",style="solid", color="black", weight=3];
540 -> 128[label="",style="dashed", color="red", weight=0];
540[label="error []",fontsize=16,color="magenta"];541 -> 472[label="",style="dashed", color="red", weight=0];
541[label="Pos Zero - Neg Zero",fontsize=16,color="magenta"];542[label="primMinusInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];542 -> 608[label="",style="solid", color="black", weight=3];
543[label="index0 (Neg Zero) (Neg (Succ wu3100)) (Pos Zero) True",fontsize=16,color="black",shape="box"];543 -> 609[label="",style="solid", color="black", weight=3];
544[label="primMinusInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];544 -> 610[label="",style="solid", color="black", weight=3];
545[label="index0 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) otherwise",fontsize=16,color="black",shape="box"];545 -> 611[label="",style="solid", color="black", weight=3];
1306[label="index1 (Pos (Succ wu35)) (Pos (Succ wu3600)) (Pos (Succ wu37)) (not (primCmpNat (Succ wu37) (Succ wu3600) == GT))",fontsize=16,color="black",shape="box"];1306 -> 1314[label="",style="solid", color="black", weight=3];
1307[label="index1 (Pos (Succ wu35)) (Pos Zero) (Pos (Succ wu37)) (not (primCmpNat (Succ wu37) Zero == GT))",fontsize=16,color="black",shape="box"];1307 -> 1315[label="",style="solid", color="black", weight=3];
1308[label="index1 (Pos (Succ wu35)) (Neg wu360) (Pos (Succ wu37)) (not True)",fontsize=16,color="black",shape="box"];1308 -> 1316[label="",style="solid", color="black", weight=3];
1557[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat (Succ wu1070) (Succ wu1080) == GT))",fontsize=16,color="black",shape="box"];1557 -> 1592[label="",style="solid", color="black", weight=3];
1558[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat (Succ wu1070) Zero == GT))",fontsize=16,color="black",shape="box"];1558 -> 1593[label="",style="solid", color="black", weight=3];
1559[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat Zero (Succ wu1080) == GT))",fontsize=16,color="black",shape="box"];1559 -> 1594[label="",style="solid", color="black", weight=3];
1560[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1560 -> 1595[label="",style="solid", color="black", weight=3];
568[label="index0 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) otherwise",fontsize=16,color="black",shape="box"];568 -> 639[label="",style="solid", color="black", weight=3];
569 -> 128[label="",style="dashed", color="red", weight=0];
569[label="error []",fontsize=16,color="magenta"];570[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="triangle"];570 -> 640[label="",style="solid", color="black", weight=3];
571 -> 128[label="",style="dashed", color="red", weight=0];
571[label="error []",fontsize=16,color="magenta"];572[label="Neg (primPlusNat Zero Zero)",fontsize=16,color="green",shape="box"];572 -> 641[label="",style="dashed", color="green", weight=3];
573[label="index0 (Pos Zero) (Neg (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];573 -> 642[label="",style="solid", color="black", weight=3];
1525 -> 1407[label="",style="dashed", color="red", weight=0];
1525[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (primCmpNat wu990 wu1000 == GT))",fontsize=16,color="magenta"];1525 -> 1561[label="",style="dashed", color="magenta", weight=3];
1525 -> 1562[label="",style="dashed", color="magenta", weight=3];
1526[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1526 -> 1563[label="",style="solid", color="black", weight=3];
1527[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1527 -> 1564[label="",style="solid", color="black", weight=3];
1528[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1528 -> 1565[label="",style="solid", color="black", weight=3];
579[label="index0 (Neg (Succ wu3000)) (Pos Zero) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];579 -> 650[label="",style="solid", color="black", weight=3];
580[label="Pos (primPlusNat Zero (Succ wu3000))",fontsize=16,color="green",shape="box"];580 -> 651[label="",style="dashed", color="green", weight=3];
581 -> 128[label="",style="dashed", color="red", weight=0];
581[label="error []",fontsize=16,color="magenta"];1359[label="index1 (Neg (Succ wu58)) (Pos wu590) (Neg (Succ wu60)) (not False)",fontsize=16,color="black",shape="box"];1359 -> 1367[label="",style="solid", color="black", weight=3];
1360[label="index1 (Neg (Succ wu58)) (Neg (Succ wu5900)) (Neg (Succ wu60)) (not (primCmpNat (Succ wu5900) (Succ wu60) == GT))",fontsize=16,color="black",shape="box"];1360 -> 1368[label="",style="solid", color="black", weight=3];
1361[label="index1 (Neg (Succ wu58)) (Neg Zero) (Neg (Succ wu60)) (not (primCmpNat Zero (Succ wu60) == GT))",fontsize=16,color="black",shape="box"];1361 -> 1369[label="",style="solid", color="black", weight=3];
600[label="primMinusInt (Neg Zero) (Neg (Succ wu3000))",fontsize=16,color="black",shape="box"];600 -> 674[label="",style="solid", color="black", weight=3];
601[label="index0 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) otherwise",fontsize=16,color="black",shape="box"];601 -> 675[label="",style="solid", color="black", weight=3];
1698 -> 1617[label="",style="dashed", color="red", weight=0];
1698[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (primCmpNat wu1120 wu1130 == GT))",fontsize=16,color="magenta"];1698 -> 1719[label="",style="dashed", color="magenta", weight=3];
1698 -> 1720[label="",style="dashed", color="magenta", weight=3];
1699[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1699 -> 1721[label="",style="solid", color="black", weight=3];
1700[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1700 -> 1722[label="",style="solid", color="black", weight=3];
1701[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1701 -> 1723[label="",style="solid", color="black", weight=3];
607[label="index0 (Neg Zero) (Pos Zero) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];607 -> 683[label="",style="solid", color="black", weight=3];
608[label="Pos (primPlusNat Zero Zero)",fontsize=16,color="green",shape="box"];608 -> 684[label="",style="dashed", color="green", weight=3];
609 -> 128[label="",style="dashed", color="red", weight=0];
609[label="error []",fontsize=16,color="magenta"];610 -> 570[label="",style="dashed", color="red", weight=0];
610[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];611[label="index0 (Neg Zero) (Neg (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];611 -> 685[label="",style="solid", color="black", weight=3];
1314 -> 1754[label="",style="dashed", color="red", weight=0];
1314[label="index1 (Pos (Succ wu35)) (Pos (Succ wu3600)) (Pos (Succ wu37)) (not (primCmpNat wu37 wu3600 == GT))",fontsize=16,color="magenta"];1314 -> 1755[label="",style="dashed", color="magenta", weight=3];
1314 -> 1756[label="",style="dashed", color="magenta", weight=3];
1314 -> 1757[label="",style="dashed", color="magenta", weight=3];
1314 -> 1758[label="",style="dashed", color="magenta", weight=3];
1314 -> 1759[label="",style="dashed", color="magenta", weight=3];
1315[label="index1 (Pos (Succ wu35)) (Pos Zero) (Pos (Succ wu37)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1315 -> 1331[label="",style="solid", color="black", weight=3];
1316 -> 1144[label="",style="dashed", color="red", weight=0];
1316[label="index1 (Pos (Succ wu35)) (Neg wu360) (Pos (Succ wu37)) False",fontsize=16,color="magenta"];1316 -> 1332[label="",style="dashed", color="magenta", weight=3];
1592 -> 1494[label="",style="dashed", color="red", weight=0];
1592[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (primCmpNat wu1070 wu1080 == GT))",fontsize=16,color="magenta"];1592 -> 1652[label="",style="dashed", color="magenta", weight=3];
1592 -> 1653[label="",style="dashed", color="magenta", weight=3];
1593[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1593 -> 1654[label="",style="solid", color="black", weight=3];
1594[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1594 -> 1655[label="",style="solid", color="black", weight=3];
1595[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1595 -> 1656[label="",style="solid", color="black", weight=3];
639[label="index0 (Pos Zero) (Pos Zero) (Pos (Succ wu400)) True",fontsize=16,color="black",shape="box"];639 -> 717[label="",style="solid", color="black", weight=3];
640[label="Pos Zero",fontsize=16,color="green",shape="box"];641[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="triangle"];641 -> 718[label="",style="solid", color="black", weight=3];
642 -> 128[label="",style="dashed", color="red", weight=0];
642[label="error []",fontsize=16,color="magenta"];1561[label="wu990",fontsize=16,color="green",shape="box"];1562[label="wu1000",fontsize=16,color="green",shape="box"];1563[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not True)",fontsize=16,color="black",shape="box"];1563 -> 1596[label="",style="solid", color="black", weight=3];
1564[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not False)",fontsize=16,color="black",shape="triangle"];1564 -> 1597[label="",style="solid", color="black", weight=3];
1565 -> 1564[label="",style="dashed", color="red", weight=0];
1565[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) (not False)",fontsize=16,color="magenta"];650 -> 128[label="",style="dashed", color="red", weight=0];
650[label="error []",fontsize=16,color="magenta"];651[label="primPlusNat Zero (Succ wu3000)",fontsize=16,color="black",shape="box"];651 -> 726[label="",style="solid", color="black", weight=3];
1367[label="index1 (Neg (Succ wu58)) (Pos wu590) (Neg (Succ wu60)) True",fontsize=16,color="black",shape="box"];1367 -> 1377[label="",style="solid", color="black", weight=3];
1368 -> 2012[label="",style="dashed", color="red", weight=0];
1368[label="index1 (Neg (Succ wu58)) (Neg (Succ wu5900)) (Neg (Succ wu60)) (not (primCmpNat wu5900 wu60 == GT))",fontsize=16,color="magenta"];1368 -> 2013[label="",style="dashed", color="magenta", weight=3];
1368 -> 2014[label="",style="dashed", color="magenta", weight=3];
1368 -> 2015[label="",style="dashed", color="magenta", weight=3];
1368 -> 2016[label="",style="dashed", color="magenta", weight=3];
1368 -> 2017[label="",style="dashed", color="magenta", weight=3];
1369[label="index1 (Neg (Succ wu58)) (Neg Zero) (Neg (Succ wu60)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1369 -> 1380[label="",style="solid", color="black", weight=3];
674[label="primMinusNat (Succ wu3000) Zero",fontsize=16,color="black",shape="triangle"];674 -> 751[label="",style="solid", color="black", weight=3];
675[label="index0 (Neg (Succ wu3000)) (Neg (Succ wu3100)) (Neg Zero) True",fontsize=16,color="black",shape="box"];675 -> 752[label="",style="solid", color="black", weight=3];
1719[label="wu1130",fontsize=16,color="green",shape="box"];1720[label="wu1120",fontsize=16,color="green",shape="box"];1721[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not True)",fontsize=16,color="black",shape="box"];1721 -> 1741[label="",style="solid", color="black", weight=3];
1722[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not False)",fontsize=16,color="black",shape="triangle"];1722 -> 1742[label="",style="solid", color="black", weight=3];
1723 -> 1722[label="",style="dashed", color="red", weight=0];
1723[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) (not False)",fontsize=16,color="magenta"];683 -> 128[label="",style="dashed", color="red", weight=0];
683[label="error []",fontsize=16,color="magenta"];684 -> 641[label="",style="dashed", color="red", weight=0];
684[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];685 -> 128[label="",style="dashed", color="red", weight=0];
685[label="error []",fontsize=16,color="magenta"];1755[label="wu37",fontsize=16,color="green",shape="box"];1756[label="wu37",fontsize=16,color="green",shape="box"];1757[label="wu3600",fontsize=16,color="green",shape="box"];1758[label="wu3600",fontsize=16,color="green",shape="box"];1759[label="wu35",fontsize=16,color="green",shape="box"];1754[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat wu118 wu119 == GT))",fontsize=16,color="burlywood",shape="triangle"];2247[label="wu118/Succ wu1180",fontsize=10,color="white",style="solid",shape="box"];1754 -> 2247[label="",style="solid", color="burlywood", weight=9];
2247 -> 1790[label="",style="solid", color="burlywood", weight=3];
2248[label="wu118/Zero",fontsize=10,color="white",style="solid",shape="box"];1754 -> 2248[label="",style="solid", color="burlywood", weight=9];
2248 -> 1791[label="",style="solid", color="burlywood", weight=3];
1331[label="index1 (Pos (Succ wu35)) (Pos Zero) (Pos (Succ wu37)) (not True)",fontsize=16,color="black",shape="box"];1331 -> 1341[label="",style="solid", color="black", weight=3];
1332[label="Neg wu360",fontsize=16,color="green",shape="box"];1652[label="wu1080",fontsize=16,color="green",shape="box"];1653[label="wu1070",fontsize=16,color="green",shape="box"];1654[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not True)",fontsize=16,color="black",shape="box"];1654 -> 1681[label="",style="solid", color="black", weight=3];
1655[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not False)",fontsize=16,color="black",shape="triangle"];1655 -> 1682[label="",style="solid", color="black", weight=3];
1656 -> 1655[label="",style="dashed", color="red", weight=0];
1656[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) (not False)",fontsize=16,color="magenta"];717 -> 128[label="",style="dashed", color="red", weight=0];
717[label="error []",fontsize=16,color="magenta"];718[label="Zero",fontsize=16,color="green",shape="box"];1596[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) False",fontsize=16,color="black",shape="box"];1596 -> 1657[label="",style="solid", color="black", weight=3];
1597[label="index1 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) True",fontsize=16,color="black",shape="box"];1597 -> 1658[label="",style="solid", color="black", weight=3];
726[label="Succ wu3000",fontsize=16,color="green",shape="box"];1377[label="Neg (Succ wu60) - Neg (Succ wu58)",fontsize=16,color="black",shape="triangle"];1377 -> 1390[label="",style="solid", color="black", weight=3];
2013[label="wu5900",fontsize=16,color="green",shape="box"];2014[label="wu58",fontsize=16,color="green",shape="box"];2015[label="wu60",fontsize=16,color="green",shape="box"];2016[label="wu5900",fontsize=16,color="green",shape="box"];2017[label="wu60",fontsize=16,color="green",shape="box"];2012[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat wu152 wu153 == GT))",fontsize=16,color="burlywood",shape="triangle"];2251[label="wu152/Succ wu1520",fontsize=10,color="white",style="solid",shape="box"];2012 -> 2251[label="",style="solid", color="burlywood", weight=9];
2251 -> 2063[label="",style="solid", color="burlywood", weight=3];
2252[label="wu152/Zero",fontsize=10,color="white",style="solid",shape="box"];2012 -> 2252[label="",style="solid", color="burlywood", weight=9];
2252 -> 2064[label="",style="solid", color="burlywood", weight=3];
1380[label="index1 (Neg (Succ wu58)) (Neg Zero) (Neg (Succ wu60)) (not False)",fontsize=16,color="black",shape="box"];1380 -> 1395[label="",style="solid", color="black", weight=3];
751[label="Pos (Succ wu3000)",fontsize=16,color="green",shape="box"];752 -> 128[label="",style="dashed", color="red", weight=0];
752[label="error []",fontsize=16,color="magenta"];1741[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) False",fontsize=16,color="black",shape="box"];1741 -> 1792[label="",style="solid", color="black", weight=3];
1742[label="index1 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) True",fontsize=16,color="black",shape="box"];1742 -> 1793[label="",style="solid", color="black", weight=3];
1790[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat (Succ wu1180) wu119 == GT))",fontsize=16,color="burlywood",shape="box"];2254[label="wu119/Succ wu1190",fontsize=10,color="white",style="solid",shape="box"];1790 -> 2254[label="",style="solid", color="burlywood", weight=9];
2254 -> 1804[label="",style="solid", color="burlywood", weight=3];
2255[label="wu119/Zero",fontsize=10,color="white",style="solid",shape="box"];1790 -> 2255[label="",style="solid", color="burlywood", weight=9];
2255 -> 1805[label="",style="solid", color="burlywood", weight=3];
1791[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat Zero wu119 == GT))",fontsize=16,color="burlywood",shape="box"];2256[label="wu119/Succ wu1190",fontsize=10,color="white",style="solid",shape="box"];1791 -> 2256[label="",style="solid", color="burlywood", weight=9];
2256 -> 1806[label="",style="solid", color="burlywood", weight=3];
2257[label="wu119/Zero",fontsize=10,color="white",style="solid",shape="box"];1791 -> 2257[label="",style="solid", color="burlywood", weight=9];
2257 -> 1807[label="",style="solid", color="burlywood", weight=3];
1341 -> 1144[label="",style="dashed", color="red", weight=0];
1341[label="index1 (Pos (Succ wu35)) (Pos Zero) (Pos (Succ wu37)) False",fontsize=16,color="magenta"];1341 -> 1350[label="",style="dashed", color="magenta", weight=3];
1681[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) False",fontsize=16,color="black",shape="box"];1681 -> 1702[label="",style="solid", color="black", weight=3];
1682[label="index1 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) True",fontsize=16,color="black",shape="box"];1682 -> 1703[label="",style="solid", color="black", weight=3];
1657[label="index0 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) otherwise",fontsize=16,color="black",shape="box"];1657 -> 1683[label="",style="solid", color="black", weight=3];
1658[label="Pos (Succ wu98) - Neg (Succ wu96)",fontsize=16,color="black",shape="box"];1658 -> 1684[label="",style="solid", color="black", weight=3];
1390[label="primMinusInt (Neg (Succ wu60)) (Neg (Succ wu58))",fontsize=16,color="black",shape="box"];1390 -> 1445[label="",style="solid", color="black", weight=3];
2063[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat (Succ wu1520) wu153 == GT))",fontsize=16,color="burlywood",shape="box"];2259[label="wu153/Succ wu1530",fontsize=10,color="white",style="solid",shape="box"];2063 -> 2259[label="",style="solid", color="burlywood", weight=9];
2259 -> 2065[label="",style="solid", color="burlywood", weight=3];
2260[label="wu153/Zero",fontsize=10,color="white",style="solid",shape="box"];2063 -> 2260[label="",style="solid", color="burlywood", weight=9];
2260 -> 2066[label="",style="solid", color="burlywood", weight=3];
2064[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat Zero wu153 == GT))",fontsize=16,color="burlywood",shape="box"];2261[label="wu153/Succ wu1530",fontsize=10,color="white",style="solid",shape="box"];2064 -> 2261[label="",style="solid", color="burlywood", weight=9];
2261 -> 2067[label="",style="solid", color="burlywood", weight=3];
2262[label="wu153/Zero",fontsize=10,color="white",style="solid",shape="box"];2064 -> 2262[label="",style="solid", color="burlywood", weight=9];
2262 -> 2068[label="",style="solid", color="burlywood", weight=3];
1395[label="index1 (Neg (Succ wu58)) (Neg Zero) (Neg (Succ wu60)) True",fontsize=16,color="black",shape="box"];1395 -> 1450[label="",style="solid", color="black", weight=3];
1792[label="index0 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) otherwise",fontsize=16,color="black",shape="box"];1792 -> 1808[label="",style="solid", color="black", weight=3];
1793[label="Pos (Succ wu111) - Neg Zero",fontsize=16,color="black",shape="box"];1793 -> 1809[label="",style="solid", color="black", weight=3];
1804[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat (Succ wu1180) (Succ wu1190) == GT))",fontsize=16,color="black",shape="box"];1804 -> 1819[label="",style="solid", color="black", weight=3];
1805[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat (Succ wu1180) Zero == GT))",fontsize=16,color="black",shape="box"];1805 -> 1820[label="",style="solid", color="black", weight=3];
1806[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat Zero (Succ wu1190) == GT))",fontsize=16,color="black",shape="box"];1806 -> 1821[label="",style="solid", color="black", weight=3];
1807[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1807 -> 1822[label="",style="solid", color="black", weight=3];
1350[label="Pos Zero",fontsize=16,color="green",shape="box"];1702[label="index0 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) otherwise",fontsize=16,color="black",shape="box"];1702 -> 1724[label="",style="solid", color="black", weight=3];
1703[label="Pos (Succ wu106) - Pos Zero",fontsize=16,color="black",shape="box"];1703 -> 1725[label="",style="solid", color="black", weight=3];
1683[label="index0 (Neg (Succ wu96)) (Pos (Succ wu97)) (Pos (Succ wu98)) True",fontsize=16,color="black",shape="box"];1683 -> 1704[label="",style="solid", color="black", weight=3];
1684[label="primMinusInt (Pos (Succ wu98)) (Neg (Succ wu96))",fontsize=16,color="black",shape="box"];1684 -> 1705[label="",style="solid", color="black", weight=3];
1445[label="primMinusNat (Succ wu58) (Succ wu60)",fontsize=16,color="black",shape="box"];1445 -> 1478[label="",style="solid", color="black", weight=3];
2065[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat (Succ wu1520) (Succ wu1530) == GT))",fontsize=16,color="black",shape="box"];2065 -> 2069[label="",style="solid", color="black", weight=3];
2066[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat (Succ wu1520) Zero == GT))",fontsize=16,color="black",shape="box"];2066 -> 2070[label="",style="solid", color="black", weight=3];
2067[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat Zero (Succ wu1530) == GT))",fontsize=16,color="black",shape="box"];2067 -> 2071[label="",style="solid", color="black", weight=3];
2068[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];2068 -> 2072[label="",style="solid", color="black", weight=3];
1450 -> 1377[label="",style="dashed", color="red", weight=0];
1450[label="Neg (Succ wu60) - Neg (Succ wu58)",fontsize=16,color="magenta"];1808[label="index0 (Neg Zero) (Pos (Succ wu110)) (Pos (Succ wu111)) True",fontsize=16,color="black",shape="box"];1808 -> 1823[label="",style="solid", color="black", weight=3];
1809[label="primMinusInt (Pos (Succ wu111)) (Neg Zero)",fontsize=16,color="black",shape="box"];1809 -> 1824[label="",style="solid", color="black", weight=3];
1819 -> 1754[label="",style="dashed", color="red", weight=0];
1819[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (primCmpNat wu1180 wu1190 == GT))",fontsize=16,color="magenta"];1819 -> 1837[label="",style="dashed", color="magenta", weight=3];
1819 -> 1838[label="",style="dashed", color="magenta", weight=3];
1820[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1820 -> 1839[label="",style="solid", color="black", weight=3];
1821[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1821 -> 1840[label="",style="solid", color="black", weight=3];
1822[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1822 -> 1841[label="",style="solid", color="black", weight=3];
1724[label="index0 (Pos Zero) (Pos (Succ wu105)) (Pos (Succ wu106)) True",fontsize=16,color="black",shape="box"];1724 -> 1743[label="",style="solid", color="black", weight=3];
1725[label="primMinusInt (Pos (Succ wu106)) (Pos Zero)",fontsize=16,color="black",shape="box"];1725 -> 1744[label="",style="solid", color="black", weight=3];
1704 -> 128[label="",style="dashed", color="red", weight=0];
1704[label="error []",fontsize=16,color="magenta"];1705[label="Pos (primPlusNat (Succ wu98) (Succ wu96))",fontsize=16,color="green",shape="box"];1705 -> 1726[label="",style="dashed", color="green", weight=3];
1478[label="primMinusNat wu58 wu60",fontsize=16,color="burlywood",shape="triangle"];2266[label="wu58/Succ wu580",fontsize=10,color="white",style="solid",shape="box"];1478 -> 2266[label="",style="solid", color="burlywood", weight=9];
2266 -> 1530[label="",style="solid", color="burlywood", weight=3];
2267[label="wu58/Zero",fontsize=10,color="white",style="solid",shape="box"];1478 -> 2267[label="",style="solid", color="burlywood", weight=9];
2267 -> 1531[label="",style="solid", color="burlywood", weight=3];
2069 -> 2012[label="",style="dashed", color="red", weight=0];
2069[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (primCmpNat wu1520 wu1530 == GT))",fontsize=16,color="magenta"];2069 -> 2073[label="",style="dashed", color="magenta", weight=3];
2069 -> 2074[label="",style="dashed", color="magenta", weight=3];
2070[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (GT == GT))",fontsize=16,color="black",shape="box"];2070 -> 2075[label="",style="solid", color="black", weight=3];
2071[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (LT == GT))",fontsize=16,color="black",shape="box"];2071 -> 2076[label="",style="solid", color="black", weight=3];
2072[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];2072 -> 2077[label="",style="solid", color="black", weight=3];
1823 -> 128[label="",style="dashed", color="red", weight=0];
1823[label="error []",fontsize=16,color="magenta"];1824[label="Pos (primPlusNat (Succ wu111) Zero)",fontsize=16,color="green",shape="box"];1824 -> 1842[label="",style="dashed", color="green", weight=3];
1837[label="wu1180",fontsize=16,color="green",shape="box"];1838[label="wu1190",fontsize=16,color="green",shape="box"];1839[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not True)",fontsize=16,color="black",shape="box"];1839 -> 1852[label="",style="solid", color="black", weight=3];
1840[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not False)",fontsize=16,color="black",shape="triangle"];1840 -> 1853[label="",style="solid", color="black", weight=3];
1841 -> 1840[label="",style="dashed", color="red", weight=0];
1841[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) (not False)",fontsize=16,color="magenta"];1743 -> 128[label="",style="dashed", color="red", weight=0];
1743[label="error []",fontsize=16,color="magenta"];1744 -> 1478[label="",style="dashed", color="red", weight=0];
1744[label="primMinusNat (Succ wu106) Zero",fontsize=16,color="magenta"];1744 -> 1794[label="",style="dashed", color="magenta", weight=3];
1744 -> 1795[label="",style="dashed", color="magenta", weight=3];
1726[label="primPlusNat (Succ wu98) (Succ wu96)",fontsize=16,color="black",shape="box"];1726 -> 1745[label="",style="solid", color="black", weight=3];
1530[label="primMinusNat (Succ wu580) wu60",fontsize=16,color="burlywood",shape="box"];2273[label="wu60/Succ wu600",fontsize=10,color="white",style="solid",shape="box"];1530 -> 2273[label="",style="solid", color="burlywood", weight=9];
2273 -> 1567[label="",style="solid", color="burlywood", weight=3];
2274[label="wu60/Zero",fontsize=10,color="white",style="solid",shape="box"];1530 -> 2274[label="",style="solid", color="burlywood", weight=9];
2274 -> 1568[label="",style="solid", color="burlywood", weight=3];
1531[label="primMinusNat Zero wu60",fontsize=16,color="burlywood",shape="box"];2275[label="wu60/Succ wu600",fontsize=10,color="white",style="solid",shape="box"];1531 -> 2275[label="",style="solid", color="burlywood", weight=9];
2275 -> 1569[label="",style="solid", color="burlywood", weight=3];
2276[label="wu60/Zero",fontsize=10,color="white",style="solid",shape="box"];1531 -> 2276[label="",style="solid", color="burlywood", weight=9];
2276 -> 1570[label="",style="solid", color="burlywood", weight=3];
2073[label="wu1530",fontsize=16,color="green",shape="box"];2074[label="wu1520",fontsize=16,color="green",shape="box"];2075[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not True)",fontsize=16,color="black",shape="box"];2075 -> 2078[label="",style="solid", color="black", weight=3];
2076[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not False)",fontsize=16,color="black",shape="triangle"];2076 -> 2079[label="",style="solid", color="black", weight=3];
2077 -> 2076[label="",style="dashed", color="red", weight=0];
2077[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) (not False)",fontsize=16,color="magenta"];1842 -> 1796[label="",style="dashed", color="red", weight=0];
1842[label="primPlusNat (Succ wu111) Zero",fontsize=16,color="magenta"];1842 -> 1854[label="",style="dashed", color="magenta", weight=3];
1842 -> 1855[label="",style="dashed", color="magenta", weight=3];
1852 -> 1144[label="",style="dashed", color="red", weight=0];
1852[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) False",fontsize=16,color="magenta"];1852 -> 1861[label="",style="dashed", color="magenta", weight=3];
1852 -> 1862[label="",style="dashed", color="magenta", weight=3];
1852 -> 1863[label="",style="dashed", color="magenta", weight=3];
1853[label="index1 (Pos (Succ wu115)) (Pos (Succ wu116)) (Pos (Succ wu117)) True",fontsize=16,color="black",shape="box"];1853 -> 1864[label="",style="solid", color="black", weight=3];
1794[label="Zero",fontsize=16,color="green",shape="box"];1795[label="Succ wu106",fontsize=16,color="green",shape="box"];1745[label="Succ (Succ (primPlusNat wu98 wu96))",fontsize=16,color="green",shape="box"];1745 -> 1796[label="",style="dashed", color="green", weight=3];
1567[label="primMinusNat (Succ wu580) (Succ wu600)",fontsize=16,color="black",shape="box"];1567 -> 1599[label="",style="solid", color="black", weight=3];
1568[label="primMinusNat (Succ wu580) Zero",fontsize=16,color="black",shape="box"];1568 -> 1600[label="",style="solid", color="black", weight=3];
1569[label="primMinusNat Zero (Succ wu600)",fontsize=16,color="black",shape="box"];1569 -> 1601[label="",style="solid", color="black", weight=3];
1570[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];1570 -> 1602[label="",style="solid", color="black", weight=3];
2078 -> 1297[label="",style="dashed", color="red", weight=0];
2078[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) False",fontsize=16,color="magenta"];2078 -> 2080[label="",style="dashed", color="magenta", weight=3];
2078 -> 2081[label="",style="dashed", color="magenta", weight=3];
2078 -> 2082[label="",style="dashed", color="magenta", weight=3];
2079[label="index1 (Neg (Succ wu149)) (Neg (Succ wu150)) (Neg (Succ wu151)) True",fontsize=16,color="black",shape="box"];2079 -> 2083[label="",style="solid", color="black", weight=3];
1854[label="Zero",fontsize=16,color="green",shape="box"];1855[label="Succ wu111",fontsize=16,color="green",shape="box"];1796[label="primPlusNat wu98 wu96",fontsize=16,color="burlywood",shape="triangle"];2281[label="wu98/Succ wu980",fontsize=10,color="white",style="solid",shape="box"];1796 -> 2281[label="",style="solid", color="burlywood", weight=9];
2281 -> 1810[label="",style="solid", color="burlywood", weight=3];
2282[label="wu98/Zero",fontsize=10,color="white",style="solid",shape="box"];1796 -> 2282[label="",style="solid", color="burlywood", weight=9];
2282 -> 1811[label="",style="solid", color="burlywood", weight=3];
1861[label="wu117",fontsize=16,color="green",shape="box"];1862[label="wu115",fontsize=16,color="green",shape="box"];1863[label="Pos (Succ wu116)",fontsize=16,color="green",shape="box"];1864[label="Pos (Succ wu117) - Pos (Succ wu115)",fontsize=16,color="black",shape="box"];1864 -> 1871[label="",style="solid", color="black", weight=3];
1599 -> 1478[label="",style="dashed", color="red", weight=0];
1599[label="primMinusNat wu580 wu600",fontsize=16,color="magenta"];1599 -> 1659[label="",style="dashed", color="magenta", weight=3];
1599 -> 1660[label="",style="dashed", color="magenta", weight=3];
1600[label="Pos (Succ wu580)",fontsize=16,color="green",shape="box"];1601[label="Neg (Succ wu600)",fontsize=16,color="green",shape="box"];1602[label="Pos Zero",fontsize=16,color="green",shape="box"];2080[label="wu151",fontsize=16,color="green",shape="box"];2081[label="Neg (Succ wu150)",fontsize=16,color="green",shape="box"];2082[label="wu149",fontsize=16,color="green",shape="box"];2083 -> 1377[label="",style="dashed", color="red", weight=0];
2083[label="Neg (Succ wu151) - Neg (Succ wu149)",fontsize=16,color="magenta"];2083 -> 2084[label="",style="dashed", color="magenta", weight=3];
2083 -> 2085[label="",style="dashed", color="magenta", weight=3];
1810[label="primPlusNat (Succ wu980) wu96",fontsize=16,color="burlywood",shape="box"];2285[label="wu96/Succ wu960",fontsize=10,color="white",style="solid",shape="box"];1810 -> 2285[label="",style="solid", color="burlywood", weight=9];
2285 -> 1825[label="",style="solid", color="burlywood", weight=3];
2286[label="wu96/Zero",fontsize=10,color="white",style="solid",shape="box"];1810 -> 2286[label="",style="solid", color="burlywood", weight=9];
2286 -> 1826[label="",style="solid", color="burlywood", weight=3];
1811[label="primPlusNat Zero wu96",fontsize=16,color="burlywood",shape="box"];2287[label="wu96/Succ wu960",fontsize=10,color="white",style="solid",shape="box"];1811 -> 2287[label="",style="solid", color="burlywood", weight=9];
2287 -> 1827[label="",style="solid", color="burlywood", weight=3];
2288[label="wu96/Zero",fontsize=10,color="white",style="solid",shape="box"];1811 -> 2288[label="",style="solid", color="burlywood", weight=9];
2288 -> 1828[label="",style="solid", color="burlywood", weight=3];
1871[label="primMinusInt (Pos (Succ wu117)) (Pos (Succ wu115))",fontsize=16,color="black",shape="box"];1871 -> 1875[label="",style="solid", color="black", weight=3];
1659[label="wu600",fontsize=16,color="green",shape="box"];1660[label="wu580",fontsize=16,color="green",shape="box"];2084[label="wu151",fontsize=16,color="green",shape="box"];2085[label="wu149",fontsize=16,color="green",shape="box"];1825[label="primPlusNat (Succ wu980) (Succ wu960)",fontsize=16,color="black",shape="box"];1825 -> 1843[label="",style="solid", color="black", weight=3];
1826[label="primPlusNat (Succ wu980) Zero",fontsize=16,color="black",shape="box"];1826 -> 1844[label="",style="solid", color="black", weight=3];
1827[label="primPlusNat Zero (Succ wu960)",fontsize=16,color="black",shape="box"];1827 -> 1845[label="",style="solid", color="black", weight=3];
1828[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1828 -> 1846[label="",style="solid", color="black", weight=3];
1875 -> 1478[label="",style="dashed", color="red", weight=0];
1875[label="primMinusNat (Succ wu117) (Succ wu115)",fontsize=16,color="magenta"];1875 -> 1900[label="",style="dashed", color="magenta", weight=3];
1875 -> 1901[label="",style="dashed", color="magenta", weight=3];
1843[label="Succ (Succ (primPlusNat wu980 wu960))",fontsize=16,color="green",shape="box"];1843 -> 1856[label="",style="dashed", color="green", weight=3];
1844[label="Succ wu980",fontsize=16,color="green",shape="box"];1845[label="Succ wu960",fontsize=16,color="green",shape="box"];1846[label="Zero",fontsize=16,color="green",shape="box"];1900[label="Succ wu115",fontsize=16,color="green",shape="box"];1901[label="Succ wu117",fontsize=16,color="green",shape="box"];1856 -> 1796[label="",style="dashed", color="red", weight=0];
1856[label="primPlusNat wu980 wu960",fontsize=16,color="magenta"];1856 -> 1865[label="",style="dashed", color="magenta", weight=3];
1856 -> 1866[label="",style="dashed", color="magenta", weight=3];
1865[label="wu960",fontsize=16,color="green",shape="box"];1866[label="wu980",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wu980), Succ(wu960)) → new_primPlusNat(wu980, wu960)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(wu980), Succ(wu960)) → new_primPlusNat(wu980, wu960)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(wu580), Succ(wu600)) → new_primMinusNat(wu580, wu600)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(wu580), Succ(wu600)) → new_primMinusNat(wu580, wu600)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index1(wu110, wu111, Succ(wu1120), Succ(wu1130)) → new_index1(wu110, wu111, wu1120, wu1130)

From the DPs we obtained the following set of size-change graphs:

new_index1(wu110, wu111, Succ(wu1120), Succ(wu1130)) → new_index1(wu110, wu111, wu1120, wu1130)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index10(wu149, wu150, wu151, Succ(wu1520), Succ(wu1530)) → new_index10(wu149, wu150, wu151, wu1520, wu1530)

From the DPs we obtained the following set of size-change graphs:

new_index10(wu149, wu150, wu151, Succ(wu1520), Succ(wu1530)) → new_index10(wu149, wu150, wu151, wu1520, wu1530)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index11(wu58, wu59, wu60, Succ(wu610), Succ(wu620)) → new_index11(wu58, wu59, wu60, wu610, wu620)

From the DPs we obtained the following set of size-change graphs:

new_index11(wu58, wu59, wu60, Succ(wu610), Succ(wu620)) → new_index11(wu58, wu59, wu60, wu610, wu620)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index12(wu96, wu97, wu98, Succ(wu990), Succ(wu1000)) → new_index12(wu96, wu97, wu98, wu990, wu1000)

From the DPs we obtained the following set of size-change graphs:

new_index12(wu96, wu97, wu98, Succ(wu990), Succ(wu1000)) → new_index12(wu96, wu97, wu98, wu990, wu1000)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index13(wu105, wu106, Succ(wu1070), Succ(wu1080)) → new_index13(wu105, wu106, wu1070, wu1080)

From the DPs we obtained the following set of size-change graphs:

new_index13(wu105, wu106, Succ(wu1070), Succ(wu1080)) → new_index13(wu105, wu106, wu1070, wu1080)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_index14(wu115, wu116, wu117, Succ(wu1180), Succ(wu1190)) → new_index14(wu115, wu116, wu117, wu1180, wu1190)

From the DPs we obtained the following set of size-change graphs:

new_index14(wu115, wu116, wu117, Succ(wu1180), Succ(wu1190)) → new_index14(wu115, wu116, wu117, wu1180, wu1190)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_index15(wu35, wu36, wu37, Succ(wu380), Succ(wu390)) → new_index15(wu35, wu36, wu37, wu380, wu390)

From the DPs we obtained the following set of size-change graphs:

new_index15(wu35, wu36, wu37, Succ(wu380), Succ(wu390)) → new_index15(wu35, wu36, wu37, wu380, wu390)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5

index1	vw vx i True	= i - vw
index1	vw vx i False	= index0 vw vx i otherwise